Merge pull request #6714 from NlightNFotis/add_new_smt_backend_label_to_regression_tests

NlightNFotis · web-flow · commit 5c3722d3caaf · 2022-03-11T11:08:59.000Z
Add new smt backend label to regression tests
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/CMakeLists.txt b/regression/cbmc/CMakeLists.txt
@@ -24,6 +24,14 @@ add_test_pl_profile(
     "CORE"
 )
 
+# If `-I` (include flag) is passed, test.pl will run only the tests matching the label following it.
+add_test_pl_profile(
+  "cbmc-new-smt-backend"
+  "$<TARGET_FILE:cbmc> --incremental-smt2-solver 'z3 --smt2 -in' --slice-formula"
+  "-I;new-smt-backend;-s;new-smt-backend"
+  "CORE"
+)
+
 # solver appears on the PATH in Windows already
 if(NOT "${CMAKE_SYSTEM_NAME}" STREQUAL "Windows")
   set_property(
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/Makefile b/regression/cbmc/Makefile
@@ -29,6 +29,11 @@ test-paths-lifo:
 					  -X thorough-paths -X smt-backend -X paths-lifo-expected-failure \
 					  -s paths-lifo $(GCC_ONLY)
 
+test-new-smt-backend:
+	@../test.pl -e -p -c "../../../src/cbmc/cbmc --incremental-smt2-solver 'z3 --smt2 -in' --slice-formula" \
+					  -I new-smt-backend \
+					  -s new-smt-backend $(GCC_ONLY)
+
 tests.log: ../test.pl test
 
 clean:
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$`