Merge pull request #7581 from tautschnig/cleanup/dedup-contracts-regression-tests

De-duplicate contracts regression tests

Author: tautschnig

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$