Merge pull request #7044 from diffblue/esteffin/cbmc-primitive-regressions

Add CBMC primitive regression tests to new SMT2 backend

Author: Enrico Steffinlongo

regression/cbmc-primitives/CMakeLists.txt

@@ -4,6 +4,14 @@ if(Z3_EXISTS)
     add_test_pl_tests(
         "$<TARGET_FILE:cbmc>"
     )
+
+    # 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"
+    )
 else()
     add_test_pl_tests(
         "$<TARGET_FILE:cbmc>" -X smt-backend

regression/cbmc-primitives/Makefile

@@ -3,6 +3,9 @@ default: tests.log
 test:
 	@../test.pl -e -p -c ../../../src/cbmc/cbmc
 
+test.smt2_incr:
+	@../test.pl -e -p -I new-smt-backend -c "../../../src/cbmc/cbmc --incremental-smt2-solver 'z3 --smt2 -in' --validate-goto-model --validate-ssa-equation --slice-formula"
+
 tests.log: ../test.pl
 	@../test.pl -e -p -c ../../../src/cbmc/cbmc
 

regression/cbmc-primitives/forall_6231_1/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 test.c
 --pointer-check
 ^EXIT=0$

regression/cbmc-primitives/forall_6231_2/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 test.c
 --pointer-check
 ^EXIT=0$

regression/cbmc-primitives/forall_6231_3/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 test.c
 --pointer-check
 ^EXIT=0$

regression/cbmc-primitives/forall_6231_3/test_malloc_less_than_bound.desc

@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 test_malloc_less_than_bound.c
 --pointer-check
 ^EXIT=10$

regression/cbmc-primitives/forall_6231_4/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 test.c
 --div-by-zero-check
 ^EXIT=10$

regression/cbmc-primitives/r_w_ok_inconsistent_invalid/test-no-cp.desc

@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 --pointer-check --no-simplify --no-propagation
 ^EXIT=0$

regression/cbmc-primitives/r_w_ok_inconsistent_invalid/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 --pointer-check
 ^EXIT=0$

regression/cbmc-primitives/r_w_ok_null/test-no-cp.desc

@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 --pointer-check --no-simplify --no-propagation
 ^EXIT=0$

regression/cbmc-primitives/r_w_ok_null/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 --pointer-check
 ^EXIT=0$

regression/cbmc-primitives/r_w_ok_valid/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 --pointer-check
 ^EXIT=0$

regression/cbmc-primitives/r_w_ok_valid_negated/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 --pointer-check
 ^EXIT=0$

regression/cbmc-primitives/same-object-01/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 
 ^EXIT=0$

regression/cbmc-primitives/same-object-02/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 
 ^EXIT=0$

regression/cbmc-primitives/same-object-03/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 
 ^EXIT=0$

regression/cbmc-primitives/same-object-04/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 
 ^EXIT=0$