Add test for address of member

regression/cbmc/address_of_struct_member/address_of.c

@@ -0,0 +1,19 @@
+struct expr
+{
+  int line;
+  char comment;
+};
+
+int main(int argc, char *argv[])
+{
+  struct expr var_expr = {42, 'a'};
+  struct expr other_expr = {34, 'b'};
+  unsigned int nondet;
+  int *ref;
+  if(nondet)
+    ref = &var_expr.line;
+  else
+    ref = &other_expr.line;
+  __CPROVER_assert(*ref != 34, "expected failure: ref == 34");
+  return 0;
+}

regression/cbmc/address_of_struct_member/test.desc

@@ -0,0 +1,9 @@
+CORE new-smt-backend
+address_of.c
+
+\[main\.assertion\.1\] line \d+ expected failure: ref == 34: FAILURE
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--