Merge pull request #8106 from esteffin/esteffin/fixing-tests-new-default-checks

Run again tests with new default checks

Author: Enrico Steffinlongo

regression/acceleration/accelerate.sh

@@ -16,7 +16,7 @@ is_windows=$4
 shift 4
 
 cfile=""
-cbmcargs="--no-standard-checks"
+cbmcargs=""
 
 # create the temporary directory relative to the current directory, thus
 # avoiding file names that start with a "/", which confuses goto-cl (Windows)

regression/acceleration/array_safe1/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
-
+--no-unwinding-assertions
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/acceleration/array_safe2/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
-
+--no-unwinding-assertions
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/acceleration/array_safe3/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
-
+--no-unwinding-assertions
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/acceleration/array_safe4/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
-
+--no-unwinding-assertions
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/acceleration/const_safe1/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
-
+--no-unwinding-assertions
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/acceleration/diamond_safe1/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
-
+--no-unwinding-assertions
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/acceleration/diamond_safe2/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
-
+--no-unwinding-assertions
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/acceleration/functions_safe1/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
-
+--no-unwinding-assertions
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/acceleration/multivar_safe1/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
-
+--no-unwinding-assertions
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/acceleration/nested_safe1/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
-
+--no-unwinding-assertions
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/acceleration/overflow_safe1/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
-
+--no-unwinding-assertions
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/acceleration/phases_safe1/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
-
+--no-unwinding-assertions
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/acceleration/simple_safe1/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
-
+--no-unwinding-assertions
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/acceleration/simple_safe2/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
-
+--no-unwinding-assertions
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/acceleration/simple_safe3/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
-
+--no-unwinding-assertions
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/acceleration/simple_safe4/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
-
+--no-unwinding-assertions
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/acceleration/underapprox_safe1/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
-
+--no-unwinding-assertions
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/acceleration/underapprox_safe2/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
-
+--no-unwinding-assertions
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/acceleration/underapprox_unsafe1/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
-
+--no-unwinding-assertions
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/acceleration/underapprox_unsafe2/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
-
+--no-unwinding-assertions
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/book-examples/CMakeLists.txt

@@ -13,27 +13,27 @@ else()
 endif()
 
 add_test_pl_tests(
-    "$<TARGET_FILE:cbmc> --no-standard-checks --validate-goto-model --validate-ssa-equation" -X smt-backend ${gcc_only} ${exclude_win_broken_tests}
+    "$<TARGET_FILE:cbmc> --validate-goto-model --validate-ssa-equation" -X smt-backend ${gcc_only} ${exclude_win_broken_tests}
 )
 
 add_test_pl_profile(
     "book-examples-paths-lifo"
-    "$<TARGET_FILE:cbmc> --no-standard-checks --paths lifo"
+    "$<TARGET_FILE:cbmc> --paths lifo"
     "-C;-X;thorough-paths;-X;smt-backend;-X;paths-lifo-expected-failure;${gcc_only_string}-s;paths-lifo;${exclude_win_broken_tests_string}"
     "CORE"
 )
 
 add_test_pl_profile(
     "book-examples-cprover-smt2"
-    "$<TARGET_FILE:cbmc> --no-standard-checks --cprover-smt2"
+    "$<TARGET_FILE:cbmc> --cprover-smt2"
     "-C;-X;broken-smt-backend;-X;thorough-smt-backend;-X;broken-cprover-smt-backend;-X;thorough-cprover-smt-backend;${gcc_only_string}-s;cprover-smt2;${exclude_win_broken_tests_string}"
     "CORE"
 )
 
 # 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> --no-standard-checks --incremental-smt2-solver 'z3 --smt2 -in'"
+  "$<TARGET_FILE:cbmc> --incremental-smt2-solver 'z3 --smt2 -in'"
   "${gcc_only_string}-X;no-new-smt;-s;new-smt-backend"
   "CORE"
 )

regression/book-examples/Makefile

@@ -10,27 +10,27 @@ GCC_ONLY =
 endif
 
 test:
-	@../test.pl -e -p -c "../../../src/cbmc/cbmc --no-standard-checks --validate-goto-model --validate-ssa-equation" -X smt-backend $(GCC_ONLY)
+	@../test.pl -e -p -c "../../../src/cbmc/cbmc --validate-goto-model --validate-ssa-equation" -X smt-backend $(GCC_ONLY)
 
 test-cprover-smt2:
-	@../test.pl -e -p -c "../../../src/cbmc/cbmc --no-standard-checks --cprover-smt2" \
+	@../test.pl -e -p -c "../../../src/cbmc/cbmc --cprover-smt2" \
 					  -X broken-smt-backend -X thorough-smt-backend \
 					  -X broken-cprover-smt-backend -X thorough-cprover-smt-backend \
 					  -s cprover-smt2 $(GCC_ONLY)
 
 test-z3:
-	@../test.pl -e -p -c "../../../src/cbmc/cbmc --no-standard-checks --z3" \
+	@../test.pl -e -p -c "../../../src/cbmc/cbmc --z3" \
 					  -X broken-smt-backend -X thorough-smt-backend \
 					  -X broken-z3-smt-backend -X thorough-z3-smt-backend \
 					  -s z3 $(GCC_ONLY)
 
 test-paths-lifo:
-	@../test.pl -e -p -c "../../../src/cbmc/cbmc --no-standard-checks --paths lifo" \
+	@../test.pl -e -p -c "../../../src/cbmc/cbmc --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 --no-standard-checks --incremental-smt2-solver 'z3 --smt2 -in'" \
+	@../test.pl -e -p -c "../../../src/cbmc/cbmc --incremental-smt2-solver 'z3 --smt2 -in'" \
 					  -X no-new-smt \
 					  -s new-smt-backend $(GCC_ONLY)
 

regression/book-examples/abs/C1.desc

@@ -1,6 +1,6 @@
 CORE
 abs.c
---function abs
+--no-signed-overflow-check --function abs
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/book-examples/lock/unwind1.desc

@@ -1,6 +1,6 @@
 CORE
 lock.c
---unwind 1
+--unwind 1 --no-unwinding-assertions
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/cbmc-concurrency/CMakeLists.txt

@@ -1,11 +1,11 @@
 if((NOT WIN32) AND (NOT APPLE) AND (NOT (CMAKE_SYSTEM_NAME STREQUAL "FreeBSD")))
 add_test_pl_tests(
-    "$<TARGET_FILE:cbmc> --no-standard-checks --validate-goto-model --validate-ssa-equation"
+    "$<TARGET_FILE:cbmc> --validate-goto-model --validate-ssa-equation"
 )
 else()
 add_test_pl_profile(
     "cbmc-concurrency"
-    "$<TARGET_FILE:cbmc> --no-standard-checks --validate-goto-model --validate-ssa-equation"
+    "$<TARGET_FILE:cbmc> --validate-goto-model --validate-ssa-equation"
     "-C;-X;pthread"
     "CORE"
 )

regression/cbmc-concurrency/Makefile

@@ -10,10 +10,10 @@ ifeq ($(filter-out OSX MSVC FreeBSD,$(BUILD_ENV_)),)
 endif
 
 test:
-	@../test.pl -e -p -c "../../../src/cbmc/cbmc --no-standard-checks --validate-goto-model --validate-ssa-equation" $(no_pthread)
+	@../test.pl -e -p -c "../../../src/cbmc/cbmc --validate-goto-model --validate-ssa-equation" $(no_pthread)
 
 tests.log: ../test.pl
-	@../test.pl -e -p -c "../../../src/cbmc/cbmc --no-standard-checks --validate-goto-model --validate-ssa-equation" $(no_pthread)
+	@../test.pl -e -p -c "../../../src/cbmc/cbmc --validate-goto-model --validate-ssa-equation" $(no_pthread)
 
 clean:
 	find . -name '*.out' -execdir $(RM) '{}' \;

regression/cbmc-concurrency/atomic_section_sc3/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
-
+--no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/cbmc-concurrency/deadlock1/test.desc

@@ -1,6 +1,6 @@
 CORE pthread
 main.c
-
+--no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/cbmc-concurrency/deadlock2/test.desc

@@ -1,6 +1,6 @@
 CORE pthread
 main.c
-
+--no-standard-checks
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

regression/cbmc-concurrency/dirty_local1/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
-
+--no-standard-checks
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

regression/cbmc-concurrency/dirty_local2/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
-
+--no-standard-checks
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

regression/cbmc-concurrency/dirty_local3/test-local.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
--Dlocals_bug
+--no-standard-checks -Dlocals_bug
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/cbmc-concurrency/dirty_local3/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
-
+--no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/cbmc-concurrency/invalid_object1/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
-
+--no-standard-checks
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

regression/cbmc-concurrency/malloc1/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
-
+--no-malloc-may-fail
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/cbmc-concurrency/malloc2/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
-
+--no-malloc-may-fail
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/cbmc-concurrency/memory_barrier1/test.desc

@@ -1,6 +1,6 @@
 CORE pthread
 main.c
---unwind 1 --no-unwinding-assertions
+--no-standard-checks --unwind 1 --no-unwinding-assertions
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/cbmc-concurrency/norace_array1/test.desc

@@ -1,6 +1,6 @@
 CORE pthread
 main.c
-
+--no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/cbmc-concurrency/norace_array2/test.desc

@@ -1,6 +1,6 @@
 CORE pthread
 main.c
-
+--no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/cbmc-concurrency/norace_scalar1/test.desc

@@ -1,6 +1,6 @@
 CORE pthread
 main.c
-
+--no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/cbmc-concurrency/norace_struct1/test.desc

@@ -1,6 +1,6 @@
 CORE pthread
 main.c
-
+--no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$