Mark some of the regression/cbmc tests with the new-smt-backend label.

NlightNFotis · NlightNFotis · commit 1004155ef2f1 · 2022-03-09T15:21:40.000Z
Now they run as part of the new `test.pl` profile added to the `CMakeLists.txt`
of the `regression/cbmc` folder, which allows us to more extensively test the
new backend, plus have the infrastructure to do so for any other test at will.
diff --git a/regression/cbmc/Associativity1/test.desc b/regression/cbmc/Associativity1/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/Assumption1/test.desc b/regression/cbmc/Assumption1/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 
 ^EXIT=10$
diff --git a/regression/cbmc/Bitfields2/test.desc b/regression/cbmc/Bitfields2/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/Fixedbv1/test.desc b/regression/cbmc/Fixedbv1/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/Fixedbv2/test.desc b/regression/cbmc/Fixedbv2/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/Fixedbv4/test.desc b/regression/cbmc/Fixedbv4/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/Fixedbv6/test.desc b/regression/cbmc/Fixedbv6/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/Fixedbv8/test.desc b/regression/cbmc/Fixedbv8/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/Function-KnR1/test.desc b/regression/cbmc/Function-KnR1/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/Function1/test.desc b/regression/cbmc/Function1/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/Function10/test.desc b/regression/cbmc/Function10/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/Function11/test.desc b/regression/cbmc/Function11/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/Function13/test.desc b/regression/cbmc/Function13/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/Function14/test.desc b/regression/cbmc/Function14/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/Function6/test.desc b/regression/cbmc/Function6/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/Function7/test.desc b/regression/cbmc/Function7/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/Function8/test.desc b/regression/cbmc/Function8/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 
 ^EXIT=10$
diff --git a/regression/cbmc/Function9/test.desc b/regression/cbmc/Function9/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 
 ^EXIT=10$
diff --git a/regression/cbmc/Function_Pointer5/test.desc b/regression/cbmc/Function_Pointer5/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/Mod1/test.desc b/regression/cbmc/Mod1/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 
 ^EXIT=10$
diff --git a/regression/cbmc/Mod2/test.desc b/regression/cbmc/Mod2/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/Negation1/test.desc b/regression/cbmc/Negation1/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/Negation2/test.desc b/regression/cbmc/Negation2/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 --no-propagation
 ^EXIT=0$
diff --git a/regression/cbmc/Nondet1/test.desc b/regression/cbmc/Nondet1/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/always_inline1/test.desc b/regression/cbmc/always_inline1/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/assert_func_four/test.desc b/regression/cbmc/assert_func_four/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 
 function .* is not declared
diff --git a/regression/cbmc/assert_lhs/test.desc b/regression/cbmc/assert_lhs/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 
 function .* is not declared
diff --git a/regression/cbmc/assert_one/test.desc b/regression/cbmc/assert_one/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 
 function .* is not declared
diff --git a/regression/cbmc/char1/test.desc b/regression/cbmc/char1/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 --unsigned-char
 ^EXIT=0$
diff --git a/regression/cbmc/cprover_assert_two/test.desc b/regression/cbmc/cprover_assert_two/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 
 ^EXIT=6$
diff --git a/regression/cbmc/exit1/test.desc b/regression/cbmc/exit1/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/for1/test.desc b/regression/cbmc/for1/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/for2/test.desc b/regression/cbmc/for2/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 
 ^EXIT=10$
diff --git a/regression/cbmc/for3/test.desc b/regression/cbmc/for3/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/goto1/test.desc b/regression/cbmc/goto1/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/goto4/test.desc b/regression/cbmc/goto4/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 --unwind 1 --unwinding-assertions
 ^EXIT=10$
diff --git a/regression/cbmc/guard1/test.desc b/regression/cbmc/guard1/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 --depth 19
 ^EXIT=0$
diff --git a/regression/cbmc/if1/test.desc b/regression/cbmc/if1/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/if3/test.desc b/regression/cbmc/if3/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 
 ^EXIT=10$
diff --git a/regression/cbmc/if4/test.desc b/regression/cbmc/if4/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/no-propagation/test.desc b/regression/cbmc/no-propagation/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 --no-propagation
 Generated 1 VCC\(s\), 1 remaining after simplification
diff --git a/regression/cbmc/noop1/test.desc b/regression/cbmc/noop1/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 -winx64
 ^EXIT=0$
diff --git a/regression/cbmc/null1/test.desc b/regression/cbmc/null1/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 --no-simplify
 ^EXIT=0$
diff --git a/regression/cbmc/null4/test.desc b/regression/cbmc/null4/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/r_w_ok4/test.desc b/regression/cbmc/r_w_ok4/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/cbmc/return1/test.desc b/regression/cbmc/return1/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/return3/test.desc b/regression/cbmc/return3/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/return4/test.desc b/regression/cbmc/return4/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
  --unwind 2
 ^EXIT=0$
diff --git a/regression/cbmc/return5/test.desc b/regression/cbmc/return5/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
  --unwind 2
 ^EXIT=10$

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`
`4`	`4`	`^EXIT=0$`