De-duplicate contracts regression tests

regression/contracts-dfcc/CMakeLists.txt

@@ -14,21 +14,28 @@ endif()
 
 
 add_test_pl_tests(
-    "${CMAKE_CURRENT_SOURCE_DIR}/chain.sh $<TARGET_FILE:goto-cc> $<TARGET_FILE:goto-instrument> $<TARGET_FILE:cbmc> ${is_windows}"
+    "${CMAKE_CURRENT_SOURCE_DIR}/chain.sh $<TARGET_FILE:goto-cc> $<TARGET_FILE:goto-instrument> $<TARGET_FILE:cbmc> ${is_windows} true"
+)
+
+add_test_pl_profile(
+    "contracts-non-dfcc"
+    "${CMAKE_CURRENT_SOURCE_DIR}/chain.sh $<TARGET_FILE:goto-cc> $<TARGET_FILE:goto-instrument> $<TARGET_FILE:cbmc> ${is_windows} false"
+    "-C;-X;dfcc-only;-s;non-dfcc"
+    "CORE"
 )
 
 ## Enabling these causes a very significant increase in the time taken to run the regressions
 
 #add_test_pl_profile(
 #    "cbmc-z3"
-#    "${CMAKE_CURRENT_SOURCE_DIR}/chain.sh $<TARGET_FILE:goto-cc> $<TARGET_FILE:goto-instrument> '$<TARGET_FILE:cbmc> --z3' ${is_windows}"
+#    "${CMAKE_CURRENT_SOURCE_DIR}/chain.sh $<TARGET_FILE:goto-cc> $<TARGET_FILE:goto-instrument> '$<TARGET_FILE:cbmc> --z3' ${is_windows} true"
 #    "-C;-X;broken-smt-backend;-X;thorough-smt-backend;-X;broken-z3-backend;-X;thorough-z3-backend;${gcc_only_string}-s;z3"
 #    "CORE"
 #)
 
 #add_test_pl_profile(
 #    "cbmc-cprover-smt2"
-#    "${CMAKE_CURRENT_SOURCE_DIR}/chain.sh $<TARGET_FILE:goto-cc> $<TARGET_FILE:goto-instrument> '$<TARGET_FILE:cbmc> --cprover-smt2' ${is_windows}"
+#    "${CMAKE_CURRENT_SOURCE_DIR}/chain.sh $<TARGET_FILE:goto-cc> $<TARGET_FILE:goto-instrument> '$<TARGET_FILE:cbmc> --cprover-smt2' ${is_windows} true"
 #    "-C;-X;broken-smt-backend;-X;thorough-smt-backend;-X;broken-cprover-smt2-backend;-X;thorough-cprover-smt2-backend;${gcc_only_string}-s;cprover-smt2"
 #    "CORE"
 #)

regression/contracts-dfcc/Makefile

@@ -14,16 +14,17 @@ else
 endif
 
 test:
-	@../test.pl -e -p -c '../chain.sh $(exe) ../../../src/goto-instrument/goto-instrument ../../../src/cbmc/cbmc $(is_windows)' -X smt-backend $(GCC_ONLY)
+	@../test.pl -e -p -c '../chain.sh $(exe) ../../../src/goto-instrument/goto-instrument ../../../src/cbmc/cbmc $(is_windows) true' -X smt-backend $(GCC_ONLY)
+	@../test.pl -e -p -c '../chain.sh $(exe) ../../../src/goto-instrument/goto-instrument ../../../src/cbmc/cbmc $(is_windows) false' -X smt-backend $(GCC_ONLY) -X dfcc-only -s non-dfcc
 
 test-cprover-smt2:
-	@../test.pl -e -p -c '../chain.sh $(exe) ../../../src/goto-instrument/goto-instrument "../../../src/cbmc/cbmc --cprover-smt2" $(is_windows)' \
+	@../test.pl -e -p -c '../chain.sh $(exe) ../../../src/goto-instrument/goto-instrument "../../../src/cbmc/cbmc --cprover-smt2" $(is_windows) true' \
 					  -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 '../chain.sh $(exe) ../../../src/goto-instrument/goto-instrument "../../../src/cbmc/cbmc --z3" $(is_windows)' \
+	@../test.pl -e -p -c '../chain.sh $(exe) ../../../src/goto-instrument/goto-instrument "../../../src/cbmc/cbmc --z3" $(is_windows) true' \
 					  -X broken-smt-backend -X thorough-smt-backend \
 					  -X broken-z3-smt-backend -X thorough-z3-smt-backend \
 					  -s z3 $(GCC_ONLY)

regression/contracts-dfcc/assigns-enforce-malloc-zero/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE dfcc-only
 main.c
 --malloc-may-fail --malloc-fail-null --dfcc main --enforce-contract foo
 ^\[foo.assigns.\d+\] line \d+ Check that a\[\(signed long (long )?int\)i\] is assignable: SUCCESS$

regression/contracts-dfcc/assigns-replace-ignored-return-value/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE dfcc-only
 main.c
 --dfcc main --replace-call-with-contract bar --replace-call-with-contract baz --enforce-contract foo
 ^EXIT=0$

regression/contracts-dfcc/assigns-replace-malloc-zero/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE dfcc-only
 main.c
 --dfcc main --replace-call-with-contract foo --malloc-may-fail --malloc-fail-null
 ^EXIT=0$

regression/contracts-dfcc/assigns_enforce_02/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE dfcc-only
 main.c
 --dfcc main --enforce-contract foo
 ^\[foo.assigns.\d+\] line 6 Check that \*x is assignable: FAILURE$

regression/contracts-dfcc/assigns_enforce_03/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE dfcc-only
 main.c
 --dfcc main --enforce-contract f1
 ^\[f3.assigns.\d+\] line 14 Check that \*x3 is assignable: SUCCESS$

regression/contracts-dfcc/assigns_enforce_04/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE dfcc-only
 main.c
 --dfcc main --enforce-contract f1
 ^\[f3.assigns.\d+\] line 13 Check that \*x3 is assignable: SUCCESS$

regression/contracts-dfcc/assigns_enforce_05/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE dfcc-only
 main.c
 --dfcc main --enforce-contract f1
 ^EXIT=0$

regression/contracts-dfcc/assigns_enforce_06/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE dfcc-only
 main.c
 --dfcc main --enforce-contract f
 ^EXIT=0$

regression/contracts-dfcc/assigns_enforce_07/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE dfcc-only
 main.c
 --dfcc main --enforce-contract f
 ^EXIT=10$

regression/contracts-dfcc/assigns_enforce_08/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE dfcc-only
 main.c
 --dfcc main --enforce-contract f1
 ^EXIT=0$

regression/contracts-dfcc/assigns_enforce_09/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE dfcc-only
 main.c
 --dfcc main --enforce-contract f1
 ^EXIT=10$

regression/contracts-dfcc/assigns_enforce_10/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE dfcc-only
 main.c
 --dfcc main --enforce-contract f1
 ^EXIT=10$

regression/contracts-dfcc/assigns_enforce_11/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE dfcc-only
 main.c
 --dfcc main --enforce-contract f1
 ^EXIT=10$

regression/contracts-dfcc/assigns_enforce_15/test-baz.desc

@@ -1,4 +1,4 @@
-CORE
+CORE dfcc-only
 main.c
 --dfcc main --enforce-contract baz
 ^\[baz.assigns.\d+\] line \d+ Check that global is assignable: FAILURE$

regression/contracts-dfcc/assigns_enforce_15/test-foo.desc

@@ -1,4 +1,4 @@
-CORE
+CORE dfcc-only
 main.c
 --dfcc main --enforce-contract foo
 ^VERIFICATION SUCCESSFUL$

regression/contracts-dfcc/assigns_enforce_15/test-qux.desc

@@ -1,4 +1,4 @@
-CORE
+CORE dfcc-only
 main.c
 --dfcc main --enforce-contract qux
 ^\[qux.assigns.\d+\] line \d+ Check that global is assignable: FAILURE$

regression/contracts-dfcc/assigns_enforce_18/test-bar.desc

@@ -1,4 +1,4 @@
-CORE
+CORE dfcc-only
 main.c
 --dfcc main --enforce-contract bar _ --pointer-primitive-check
 ^\[bar.assigns.\d+\] line 20 Check that \*b is assignable: SUCCESS$

regression/contracts-dfcc/assigns_enforce_18/test-baz.desc

@@ -1,4 +1,4 @@
-CORE
+CORE dfcc-only
 main.c
 --dfcc main --enforce-contract baz _ --pointer-primitive-check
 ^\[free.frees.\d+\].*Check that ptr is freeable: FAILURE

regression/contracts-dfcc/assigns_enforce_18/test-foo.desc

@@ -1,4 +1,4 @@
-CORE
+CORE dfcc-only
 main.c
 --dfcc main --enforce-contract foo _ --pointer-primitive-check
 ^\[foo.assigns.\d+\] line 13 Check that \*xp is assignable: SUCCESS$

regression/contracts-dfcc/assigns_enforce_19_a/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE dfcc-only
 main.c
 --dfcc main --enforce-contract f
 ^\[f.assigns.\d+\] .* Check that a is assignable: SUCCESS$

regression/contracts-dfcc/assigns_enforce_19_b/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE dfcc-only
 main.c
 --dfcc main --enforce-contract f
 ^\[f.assigns.\d+\] line \d+ Check that b is assignable: SUCCESS$

regression/contracts-dfcc/assigns_enforce_20/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE dfcc-only
 main.c
 --dfcc main --enforce-contract foo
 ^EXIT=10$

regression/contracts-dfcc/assigns_enforce_21/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE dfcc-only
 main.c
 --dfcc main --enforce-contract foo --replace-call-with-contract quz
 ^\[bar.assigns.\d+\].*Check that \*y is assignable: SUCCESS$

regression/contracts-dfcc/assigns_enforce_arrays_02/test-f1.desc

@@ -1,4 +1,4 @@
-CORE
+CORE dfcc-only
 main.c
 --dfcc main --enforce-contract f1
 ^\[f1.assigns.\d+\] line 8 Check that a\[.*0\] is assignable: SUCCESS$

regression/contracts-dfcc/assigns_enforce_arrays_02/test-f2.desc

@@ -1,4 +1,4 @@
-CORE
+CORE dfcc-only
 main.c
 --dfcc main --enforce-contract f2
 ^\[f2.assigns.\d+\] line \d+ Check that a\[.*0\] is assignable: SUCCESS$

regression/contracts-dfcc/assigns_enforce_arrays_05/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE dfcc-only
 main.c
 --dfcc main --enforce-contract uses_assigns
 ^\[assigns_ptr.assigns.\d+\] line \d+ Check that \*x is assignable: SUCCESS$

regression/contracts-dfcc/assigns_enforce_arrays_10/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE dfcc-only
 main.c
 --dfcc main --enforce-contract f1
 ^EXIT=10$

regression/contracts-dfcc/assigns_enforce_conditional_function_call_condition/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE dfcc-only
 main.c
 --dfcc main --enforce-contract foo
 ^main.c function foo$

regression/contracts-dfcc/assigns_enforce_conditional_lvalue/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE dfcc-only
 main.c
 --dfcc main --enforce-contract foo
 main.c function foo

regression/contracts-dfcc/assigns_enforce_conditional_lvalue_list/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE dfcc-only
 main.c
 --dfcc main --enforce-contract foo
 main.c function foo

regression/contracts-dfcc/assigns_enforce_conditional_pointer_object/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE dfcc-only
 main.c
 --dfcc main --enforce-contract foo
 main.c function foo

regression/contracts-dfcc/assigns_enforce_conditional_pointer_object_list/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE dfcc-only
 main.c
 --dfcc main --enforce-contract foo
 main.c function foo

regression/contracts-dfcc/assigns_enforce_conditional_unions/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE dfcc-only
 main.c
 --dfcc main --enforce-contract update _ --pointer-check --pointer-overflow-check --signed-overflow-check --unsigned-overflow-check --conversion-check
 ^\[is_high_level.assigns.\d+\] line 52 Check that latch is assignable: SUCCESS$

regression/contracts-dfcc/assigns_enforce_detect_local_statics/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE dfcc-only
 main.c
 --dfcc main --enforce-contract bar
 ^\[foo.assigns.\d+\] line 17 Check that \*y is assignable: SUCCESS$

regression/contracts-dfcc/assigns_enforce_detect_replaced_local_statics/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE dfcc-only
 main.c
 --dfcc main --replace-call-with-contract bar --replace-call-with-contract baz --enforce-contract foo _ --pointer-check
 ^\[main.assertion.\d+\] line \d+ expecting FAILURE: FAILURE$

regression/contracts-dfcc/assigns_enforce_free_dead/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE dfcc-only
 main.c
 --malloc-may-fail --malloc-fail-null --dfcc main --enforce-contract foo _ --pointer-primitive-check
 ^\[foo.assigns.\d+\] line 6 Check that \*x is assignable: SUCCESS$

regression/contracts-dfcc/assigns_enforce_havoc_object/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE dfcc-only
 main.c
 --dfcc main --enforce-contract foo
 ^EXIT=10$

regression/contracts-dfcc/assigns_enforce_malloc_02/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE dfcc-only
 main.c
 --dfcc main --enforce-contract f
 main.c function f

regression/contracts-dfcc/assigns_enforce_multi_file_02/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE dfcc-only
 main.c
 --dfcc main --enforce-contract f1
 ^EXIT=0$

regression/contracts-dfcc/assigns_enforce_offsets_2/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE dfcc-only
 main.c
 --dfcc main --enforce-contract foo _ --pointer-check
 ^\[foo.assigns.*\d+\].* line 8 Check that x\[\(.*\)1\] is assignable: (SUCCESS|FAILURE)$

regression/contracts-dfcc/assigns_enforce_offsets_4/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE dfcc-only
 main.c
 --dfcc main --enforce-contract foo _ --pointer-check
 ^EXIT=10$

regression/contracts-dfcc/assigns_enforce_scoping_01/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE dfcc-only
 main.c
 --dfcc main --enforce-contract f1
 ^EXIT=10$

regression/contracts-dfcc/assigns_enforce_scoping_02/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE dfcc-only
 main.c
 --dfcc main --enforce-contract f1
 ^EXIT=10$

regression/contracts-dfcc/assigns_enforce_statics/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE dfcc-only
 main.c
 --dfcc main --enforce-contract foo _ --pointer-primitive-check
 ^\[foo.assigns.\d+\] line \d+ Check that y is assignable: SUCCESS$

regression/contracts-dfcc/assigns_enforce_structs_04/test-f1.desc

@@ -1,4 +1,4 @@
-CORE
+CORE dfcc-only
 main.c
 --dfcc main --enforce-contract f1
 ^EXIT=10$

regression/contracts-dfcc/assigns_enforce_structs_04/test-f2.desc

@@ -1,4 +1,4 @@
-CORE
+CORE dfcc-only
 main.c
 --dfcc main --enforce-contract f2
 ^EXIT=10$

regression/contracts-dfcc/assigns_enforce_structs_04/test-f3.desc

@@ -1,4 +1,4 @@
-CORE
+CORE dfcc-only
 main.c
 --dfcc main --enforce-contract f3
 ^EXIT=0$

regression/contracts-dfcc/assigns_enforce_structs_04/test-f4.desc

@@ -1,4 +1,4 @@
-CORE
+CORE dfcc-only
 main.c
 --dfcc main --enforce-contract f4
 ^EXIT=0$

regression/contracts-dfcc/assigns_enforce_structs_06/test-f1.desc

@@ -1,4 +1,4 @@
-CORE
+CORE dfcc-only
 main.c
 --dfcc main --enforce-contract f1
 ^EXIT=10$

regression/contracts-dfcc/assigns_enforce_structs_06/test-f2.desc

@@ -1,4 +1,4 @@
-CORE
+CORE dfcc-only
 main.c
 --dfcc main --enforce-contract f2
 ^EXIT=10$

regression/contracts-dfcc/assigns_enforce_structs_06/test-f3.desc

@@ -1,4 +1,4 @@
-CORE
+CORE dfcc-only
 main.c
 --dfcc main --enforce-contract f3
 ^EXIT=0$

regression/contracts-dfcc/assigns_enforce_structs_07/test-f1.desc

@@ -1,4 +1,4 @@
-CORE
+CORE dfcc-only
 main.c
 --malloc-may-fail --malloc-fail-null --dfcc main --enforce-contract f1 _ --pointer-check
 ^EXIT=10$

regression/contracts-dfcc/assigns_enforce_structs_07/test-f2.desc

@@ -1,4 +1,4 @@
-CORE
+CORE dfcc-only
 main.c
 --malloc-may-fail --malloc-fail-null --dfcc main --enforce-contract f2 _ --pointer-check
 ^EXIT=10$

regression/contracts-dfcc/assigns_enforce_structs_08/test-f1.desc

@@ -1,4 +1,4 @@
-CORE
+CORE dfcc-only
 main.c
 --dfcc main --enforce-contract f1 _ --malloc-may-fail --malloc-fail-null --pointer-check
 ^\[f1.assigns.\d+\] line \d+ Check that p->buf\[\(.*\)0\] is assignable: SUCCESS$

regression/contracts-dfcc/assigns_enforce_structs_08/test-f2.desc

@@ -1,4 +1,4 @@
-CORE
+CORE dfcc-only
 main.c
 --dfcc main --enforce-contract f2 _ --malloc-may-fail --malloc-fail-null --pointer-check
 ^\[f2.assigns.\d+\] line \d+ Check that pp->p->buf\[\(.*\)0\] is assignable: SUCCESS$

regression/contracts-dfcc/assigns_enforce_subfunction_calls/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE dfcc-only
 main.c
 --dfcc main --enforce-contract foo
 ^\[baz.assigns.\d+\].*Check that \*x is assignable: FAILURE$

regression/contracts-dfcc/assigns_repeated_ignored/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE dfcc-only
 main.c
 --dfcc main --enforce-contract foo
 ^VERIFICATION SUCCESSFUL$