Add regression test for nested struct member

diffblue · Oct 6, 2023 · eadb111 · eadb111
1 parent 7de085d
commit eadb111
Show file tree

Hide file tree

Showing 4 changed files with 37 additions and 2 deletions.
diff --git a/regression/cbmc/Struct_Initialization5/test.desc b/regression/cbmc/Struct_Initialization5/test.desc
@@ -1,4 +1,4 @@
-CORE new-smt-backend
+CORE
 main.c
 
 ^EXIT=0$

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$
+--
+--
diff --git a/regression/cbmc/struct16/test.desc b/regression/cbmc/struct16/test.desc
@@ -1,4 +1,4 @@
-CORE new-smt-backend
+CORE
 main.c
 
 ^VERIFICATION SUCCESSFUL$