Merge pull request #6244 from martin-cs/fix/tag-z3-regression-tests-3

Mark a test that uses --smt2 as needing the smt-backend

Author: martin-cs

regression/Makefile

@@ -47,7 +47,7 @@ DIRS = cbmc \
        cbmc-primitives \
        goto-interpreter \
        cbmc-sequentialization \
-			 cpp-linter \
+       cpp-linter \
        # Empty last line
 
 ifeq ($(OS),Windows_NT)

regression/cbmc/issue_5952_soundness_bug_smt_encoding/test_short.desc

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

regression/contracts/CMakeLists.txt

@@ -4,6 +4,40 @@ else()
   set(is_windows false)
 endif()
 
+if("${CMAKE_CXX_COMPILER_ID}" STREQUAL "MSVC")
+  set(gcc_only -X gcc-only)
+  set(gcc_only_string "-X;gcc-only;")
+else()
+  set(gcc_only "")
+  set(gcc_only_string "")
+endif()
+
+
 add_test_pl_tests(
     "${CMAKE_CURRENT_SOURCE_DIR}/chain.sh $<TARGET_FILE:goto-cc> $<TARGET_FILE:goto-instrument> $<TARGET_FILE:cbmc> ${is_windows}"
 )
+
+## 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}"
+#    "-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}"
+#    "-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"
+#)
+
+# solver appears on the PATH in Windows already
+#if(NOT "${CMAKE_SYSTEM_NAME}" STREQUAL "Windows")
+#  set_property(
+#    TEST "cbmc-cprover-smt2-CORE"
+#    PROPERTY ENVIRONMENT
+#      "PATH=$ENV{PATH}:$<TARGET_FILE_DIR:smt2_solver>"
+#  )
+#endif()

regression/contracts/Makefile

@@ -1,28 +1,42 @@
-default: tests.log
+default: test
 
 include ../../src/config.inc
 include ../../src/common
 
 ifeq ($(BUILD_ENV_),MSVC)
 	exe=../../../src/goto-cc/goto-cl
 	is_windows=true
+	GCC_ONLY = -X gcc-only
 else
 	exe=../../../src/goto-cc/goto-cc
 	is_windows=false
+	GCC_ONLY =
 endif
 
 test:
-	@../test.pl -e -p -c '../chain.sh $(exe) ../../../src/goto-instrument/goto-instrument ../../../src/cbmc/cbmc $(is_windows)'
+	@../test.pl -e -p -c '../chain.sh $(exe) ../../../src/goto-instrument/goto-instrument ../../../src/cbmc/cbmc $(is_windows)' -X smt-backend $(GCC_ONLY)
+
+test-cprover-smt2:
+	@../test.pl -e -p -c '../chain.sh $(exe) ../../../src/goto-instrument/goto-instrument "../../../src/cbmc/cbmc --cprover-smt2" $(is_windows)' \
+					  -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)' \
+					  -X broken-smt-backend -X thorough-smt-backend \
+					  -X broken-z3-smt-backend -X thorough-z3-smt-backend \
+					  -s z3 $(GCC_ONLY)
+
+tests.log: ../test.pl test
 
-tests.log:
-	@../test.pl -e -p -c '../chain.sh $(exe) ../../../src/goto-instrument/goto-instrument ../../../src/cbmc/cbmc $(is_windows)'
 
 clean:
 	@for dir in *; do \
 		$(RM) tests.log; \
 		if [ -d "$$dir" ]; then \
 			cd "$$dir"; \
-			$(RM) *.out *.gb; \
+			$(RM) *.out *.gb *.smt2; \
 			cd ..; \
 		fi \
 	done

regression/contracts/quantifiers-loop-02/test.desc

@@ -1,4 +1,4 @@
-CORE smt-backend
+CORE smt-backend broken-cprover-smt-backend
 main.c
 --apply-loop-contracts _ --z3
 ^EXIT=0$
@@ -14,9 +14,5 @@ This test case checks the handling of a universal quantifier, with a symbolic
 upper bound, within a loop invariant.
 
 TODO: This test should:
-- be tagged `smt-backend`:
-  because the SAT backend does not support (simply ignores) `forall` in negative (e.g. assume) contexts.
-- be tagged `broken-cprover-smt-backend`:
-  because the CPROVER SMT2 solver cannot handle (errors out on) `forall` in negative (e.g. assume) contexts.
 - not use the `_ --z3` parameters:
   once SMT-related tags are supported by the `Makefile`.