Activate all struct tests from regression/cbmc/

NlightNFotis · NlightNFotis · commit de9340c4b6fa · 2023-10-06T15:02:55.000+01:00
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_Initialization5/test.desc b/regression/cbmc/Struct_Initialization5/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/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/struct16/test.desc b/regression/cbmc/struct16/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 
 ^VERIFICATION SUCCESSFUL$
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$`