Merge pull request #8002 from thomasspriggs/tas/smt-test-flip

Replace `new-smt-backend` tag with inverted `no-new-smt` tag

Author: thomasspriggs

regression/book-examples/CMakeLists.txt

@@ -30,11 +30,11 @@ add_test_pl_profile(
     "CORE"
 )
 
-# If `-I` (include flag) is passed, test.pl will run only the tests matching the label following it.
+# If `-X` (exclude flag) is passed, test.pl will exclude the tests matching the label following it.
 add_test_pl_profile(
   "book-examples-new-smt-backend"
   "$<TARGET_FILE:cbmc> --incremental-smt2-solver 'z3 --smt2 -in'"
-  "${gcc_only_string}-I;new-smt-backend;-s;new-smt-backend"
+  "${gcc_only_string}-X;no-new-smt;-s;new-smt-backend"
   "CORE"
 )
 

regression/book-examples/Makefile

@@ -31,7 +31,7 @@ test-paths-lifo:
 
 test-new-smt-backend:
 	@../test.pl -e -p -c "../../../src/cbmc/cbmc --incremental-smt2-solver 'z3 --smt2 -in'" \
-					  -I new-smt-backend \
+					  -X no-new-smt \
 					  -s new-smt-backend $(GCC_ONLY)
 
 tests.log: ../test.pl test

regression/book-examples/abs/C1.desc

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

regression/book-examples/abs/C13.desc

@@ -1,4 +1,4 @@
-CORE new-smt-backend
+CORE
 abs.c
 --function abs --signed-overflow-check --show-goto-functions
 ^EXIT=0$

regression/book-examples/abs/C2.desc

@@ -1,4 +1,4 @@
-CORE new-smt-backend
+CORE
 abs.c
 --function abs --signed-overflow-check
 ^EXIT=10$

regression/book-examples/abs/C3.desc

@@ -1,4 +1,4 @@
-CORE new-smt-backend
+CORE
 abs.c
 --function abs --signed-overflow-check --trace
 ^EXIT=10$

regression/book-examples/binsearch/C4.desc

@@ -1,4 +1,4 @@
-CORE new-smt-backend
+CORE
 binsearch.c
 --function binsearch --unwind 6 --bounds-check --unwinding-assertions
 ^EXIT=0$

regression/book-examples/lock/depth.desc

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

regression/book-examples/lock/unwind1.desc

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

regression/book-examples/lock/unwind2.desc

@@ -1,4 +1,4 @@
-CORE new-smt-backend
+CORE
 lock.c
 --unwind 2
 ^EXIT=10$

regression/book-examples/login/C5.desc

@@ -1,4 +1,4 @@
-CORE new-smt-backend
+CORE
 login.c
 --unwind 20 --bounds-check
 ^EXIT=10$

regression/book-examples/login/C6.desc

@@ -1,4 +1,4 @@
-CORE new-smt-backend
+CORE
 login.c
 --show-properties --bounds-check --pointer-check
 ^EXIT=0$

regression/book-examples/login/C7.desc

@@ -1,4 +1,4 @@
-CORE new-smt-backend
+CORE
 login.c
 --unwind 20 --show-vcc --bounds-check --pointer-check
 ^EXIT=0$

regression/book-examples/login/C8.desc

@@ -1,4 +1,4 @@
-CORE new-smt-backend
+CORE
 login.c
 --unwind 20 --bounds-check --pointer-check
 ^EXIT=10$

regression/book-examples/login/C9.desc

@@ -1,4 +1,4 @@
-CORE new-smt-backend
+CORE
 login.c
 --unwind 20 --bounds-check --pointer-check --trace
 ^EXIT=10$

regression/book-examples/pid/C11.desc

@@ -1,4 +1,4 @@
-CORE
+CORE no-new-smt
 pid.c
 --cover mcdc --unwind 6
 ^EXIT=0$

regression/cbmc-primitives/CMakeLists.txt

@@ -5,11 +5,11 @@ if(Z3_EXISTS)
         "$<TARGET_FILE:cbmc>"
     )
 
-    # If `-I` (include flag) is passed, test.pl will run only the tests matching the label following it.
+    # If `-X` (exclude flag) is passed, test.pl will exclude the tests matching the label following it.
     add_test_pl_profile(
             "cbmc-primitives-new-smt-backend"
             "$<TARGET_FILE:cbmc> --incremental-smt2-solver 'z3 --smt2 -in'"
-            "-I;new-smt-backend;-s;new-smt-backend"
+            "-X;no-new-smt;-s;new-smt-backend"
             "CORE"
     )
 else()

regression/cbmc-primitives/Makefile

@@ -4,7 +4,7 @@ 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"
+	@../test.pl -e -p -X no-new-smt -c "../../../src/cbmc/cbmc --incremental-smt2-solver 'z3 --smt2 -in' --validate-goto-model --validate-ssa-equation"
 
 tests.log: ../test.pl
 	@../test.pl -e -p -c ../../../src/cbmc/cbmc

regression/cbmc-primitives/alternating_quantifiers_6231/exists_in_forall.desc

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

regression/cbmc-primitives/alternating_quantifiers_6231/forall_in_exists.desc

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

regression/cbmc-primitives/dynamic-object-02/test-no-cp.desc

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

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

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

regression/cbmc-primitives/exists_assume_6231/test.desc

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

regression/cbmc-primitives/exists_assume_6231/test2.desc

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

regression/cbmc-primitives/exists_memory_checks/invalid_index_range.desc

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

regression/cbmc-primitives/exists_memory_checks/negated_exists.desc

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

regression/cbmc-primitives/exists_memory_checks/smt_missing_range_check.desc

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

regression/cbmc-primitives/exists_memory_checks/valid_index_range.desc

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

regression/cbmc-primitives/forall_6231_1/test.desc

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

regression/cbmc-primitives/forall_6231_2/test.desc

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

regression/cbmc-primitives/forall_6231_3/test.desc

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

regression/cbmc-primitives/forall_6231_3/test_malloc_less_than_bound.desc

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

regression/cbmc-primitives/forall_6231_4/test.desc

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

regression/cbmc-primitives/implication_statement_checks_1/test.desc

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

regression/cbmc-primitives/pointer-offset-01/test-no-cp.desc

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

regression/cbmc-primitives/pointer-offset-01/test.desc

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

regression/cbmc-primitives/r_w_ok_bug/test.desc

@@ -1,4 +1,4 @@
-CORE new-smt-backend
+CORE
 main.c
 --pointer-check --no-simplify --no-propagation
 ^\[main.pointer_dereference.\d+\] line 8 dereference failure: pointer outside object bounds in \*p1: FAILURE$

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

@@ -1,4 +1,4 @@
-CORE new-smt-backend
+CORE
 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 new-smt-backend
+CORE
 main.c
 --pointer-check
 ^EXIT=0$

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

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

regression/cbmc-primitives/r_w_ok_null/test.desc

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

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

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

regression/cbmc-primitives/r_w_ok_valid/test.desc

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

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

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

regression/cbmc-primitives/r_w_ok_valid_negated/test.desc

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

regression/cbmc/ACSL/operators.desc

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

regression/cbmc/ACSL/quantifier-precedence.desc

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

regression/cbmc/ASHR1/test.desc

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

regression/cbmc/Address_of1/test.desc

@@ -1,4 +1,4 @@
-CORE new-smt-backend
+CORE
 main.c
 --stop-on-fail
 ^\[main\.assertion

regression/cbmc/Address_of2/test.desc

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

regression/cbmc/Anonymous_Struct1/test.desc

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

regression/cbmc/Anonymous_Struct2/test.desc

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

regression/cbmc/Anonymous_Struct3/test.desc

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

regression/cbmc/Array_Access1/test.desc

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

regression/cbmc/Array_Access2/test.desc

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