Add regression test for nested struct member

diffblue · Jul 18, 2023 · 16b0492 · 16b0492
1 parent a7ff65a
commit 16b0492
Show file tree

Hide file tree

Showing 2 changed files with 35 additions and 0 deletions.
diff --git a/regression/cbmc/address_of_struct_member_rec/address_of_rec.c b/regression/cbmc/address_of_struct_member_rec/address_of_rec.c
@@ -0,0 +1,26 @@
+struct aux
+{
+  char comment;
+};
+
+struct expr
+{
+  int line;
+  struct aux *info;
+};
+
+int main(void)
+{
+  struct aux info1 = {'a'};
+  struct aux info2 = {'b'};
+  struct expr var_expr = {42, &info1};
+  struct expr other_expr = {34, &info2};
+  unsigned int nondet;
+  char *ref;
+  if(nondet)
+    ref = &var_expr.info->comment;
+  else
+    ref = &other_expr.info->comment;
+  __CPROVER_assert(*ref != 'b', "expected failure: ref == 'b'");
+  return 0;
+}
diff --git a/regression/cbmc/address_of_struct_member_rec/test.desc b/regression/cbmc/address_of_struct_member_rec/test.desc
@@ -0,0 +1,9 @@
+CORE new-smt-backend
+address_of_rec.c
+
+\[main\.assertion\.1\] line \d+ expected failure: ref == 'b': FAILURE
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--