Merge pull request #7809 from NlightNFotis/address_of_field

thomasspriggs · web-flow · commit cf380d55c551 · 2023-10-10T14:54:08.000+01:00
Enable all struct tests under `regression/cbmc/` for new SMT backend
diff --git a/regression/cbmc/Anonymous_Struct1/test.desc b/regression/cbmc/Anonymous_Struct1/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 --pointer-check
 ^EXIT=0$
diff --git a/regression/cbmc/Anonymous_Struct2/test.desc b/regression/cbmc/Anonymous_Struct2/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/Anonymous_Struct3/test.desc b/regression/cbmc/Anonymous_Struct3/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 -win32
 ^EXIT=0$
diff --git a/regression/cbmc/Struct_Array1/test.desc b/regression/cbmc/Struct_Array1/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/Struct_Bytewise1/test.desc b/regression/cbmc/Struct_Bytewise1/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 struct_bytewise.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/Struct_Bytewise2/test.desc b/regression/cbmc/Struct_Bytewise2/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/Struct_Initialization1/test.desc b/regression/cbmc/Struct_Initialization1/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/Struct_Initialization10/test.desc b/regression/cbmc/Struct_Initialization10/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/Struct_Initialization2/test.desc b/regression/cbmc/Struct_Initialization2/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/Struct_Initialization3/test.desc b/regression/cbmc/Struct_Initialization3/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/Struct_Initialization4/test.desc b/regression/cbmc/Struct_Initialization4/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/Struct_Initialization6/test.desc b/regression/cbmc/Struct_Initialization6/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/Struct_Initialization7/test.desc b/regression/cbmc/Struct_Initialization7/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/Struct_Initialization8/test.desc b/regression/cbmc/Struct_Initialization8/test.desc
@@ -1,4 +1,4 @@
-FUTURE
+CORE new-smt-backend
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/Struct_Initialization9/test.desc b/regression/cbmc/Struct_Initialization9/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/Struct_Padding1/test.desc b/regression/cbmc/Struct_Padding1/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.i
 --32
 ^EXIT=0$
diff --git a/regression/cbmc/Struct_Pointer1/test.desc b/regression/cbmc/Struct_Pointer1/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/Struct_Pointer2/test.desc b/regression/cbmc/Struct_Pointer2/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 --pointer-check
 ^EXIT=0$
diff --git a/regression/cbmc/Struct_Pointer3/test.desc b/regression/cbmc/Struct_Pointer3/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/Struct_Pointer_Array1/test.desc b/regression/cbmc/Struct_Pointer_Array1/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/Struct_Propagation1/test.desc b/regression/cbmc/Struct_Propagation1/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 --unwind 5
 ^EXIT=0$
diff --git a/regression/cbmc/address_of_struct_member/address_of.c b/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;
+}
diff --git a/regression/cbmc/address_of_struct_member/test.desc b/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$
+--
+--
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/struct1/test.desc b/regression/cbmc/struct1/test.desc
@@ -1,4 +1,4 @@
-CORE gcc-only
+CORE gcc-only new-smt-backend
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/struct10/test.desc b/regression/cbmc/struct10/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/struct11/test.desc b/regression/cbmc/struct11/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/struct12/test.desc b/regression/cbmc/struct12/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 --pointer-check --bounds-check
 ^EXIT=0$
diff --git a/regression/cbmc/struct13/test.desc b/regression/cbmc/struct13/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/struct14/test.desc b/regression/cbmc/struct14/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 
 ^EXIT=10$
diff --git a/regression/cbmc/struct15/test.desc b/regression/cbmc/struct15/test.desc
@@ -1,4 +1,4 @@
-CORE smt-backend
+CORE smt-backend new-smt-backend
 main.c
 --trace --z3
 ^EXIT=0$
diff --git a/regression/cbmc/struct17/test.desc b/regression/cbmc/struct17/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/cbmc/struct3/test.desc b/regression/cbmc/struct3/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/struct4/test.desc b/regression/cbmc/struct4/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/struct6/test.desc b/regression/cbmc/struct6/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 --bounds-check --pointer-check
 ^EXIT=0$
diff --git a/regression/cbmc/struct7/test.desc b/regression/cbmc/struct7/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 --pointer-check --bounds-check
 ^EXIT=0$
diff --git a/regression/cbmc/struct8/test.desc b/regression/cbmc/struct8/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/struct9/test.desc b/regression/cbmc/struct9/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 
 ^EXIT=0$

Original file line number	Diff line number	Diff line change
`@@ -1,4 +1,4 @@`
`1`		`-CORE`
	`1`	`+CORE new-smt-backend`
`2`	`2`	`main.c`
`3`	`3`	`--pointer-check`
`4`	`4`	`^EXIT=0$`