Cleanup of SMT2 solver test execution and CMake support [blocks: #4063]

.travis.yml

@@ -304,7 +304,7 @@ script:
   - if [ -e bin/gcc ] ; then export PATH=$PWD/bin:$PATH ; fi ;
   - env UBSAN_OPTIONS=print_stacktrace=1 make -C regression test-parallel "CXX=${COMPILER} ${EXTRA_CXXFLAGS}" -j2 JOBS=2
   - UBSAN_OPTIONS=print_stacktrace=1 make -C regression/cbmc test-paths-lifo
-  - scripts/delete_failing_smt2_solver_tests ; env PATH=$PATH:`pwd`/src/solvers UBSAN_OPTIONS=print_stacktrace=1 make -C regression/cbmc test-cprover-smt2
+  - env PATH=$PATH:`pwd`/src/solvers UBSAN_OPTIONS=print_stacktrace=1 make -C regression/cbmc test-cprover-smt2
   - make -C unit "CXX=${COMPILER} ${EXTRA_CXXFLAGS}" -j2
   - make -C unit test
   - env UBSAN_OPTIONS=print_stacktrace=1 make -C jbmc/regression test-parallel "CXX=${COMPILER} ${EXTRA_CXXFLAGS}" -j2 JOBS=2

CODEOWNERS

@@ -60,7 +60,6 @@
 /jbmc/regression/
 
 /scripts/ @diffblue/devops @thk123 @forejtv @peterschrammel
-/scripts/delete_failing_smt2_solver_tests
 /scripts/expected_doxygen_warnings.txt
 
 /.travis.yml @diffblue/devops @thk123 @forejtv @peterschrammel @chrisr-diffblue

buildspec-linux-clang.yml

@@ -22,7 +22,6 @@ phases:
     commands:
       - make -C unit test CXX='ccache /usr/bin/clang++-7' CXX_FLAGS='-Qunused-arguments'
       - make -C regression test
-      - scripts/delete_failing_smt2_solver_tests
       - env PATH=$PATH:`pwd`/src/solvers make -C regression/cbmc test-cprover-smt2
       - make -C jbmc/unit test CXX='ccache /usr/bin/clang++-7' CXX_FLAGS='-Qunused-arguments'
       - make -C jbmc/regression test

buildspec-windows.yml

@@ -40,6 +40,10 @@ phases:
         $env:Path = "C:\tools\cygwin\bin;$env:Path"
         cmd /c 'call "C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\vcvarsall.bat" x64 && bash -c "make -C regression test BUILD_ENV=MSVC" '
 
+      - |
+        $env:Path = "$pwd\src\solvers;C:\tools\cygwin\bin;$env:Path"
+        cmd /c 'call "C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\vcvarsall.bat" x64 && bash -c "make -C regression/cbmc test-cprover-smt2 BUILD_ENV=MSVC" '
+
       - |
         $env:Path = "C:\tools\cygwin\bin;$env:Path"
         cmd /c 'call "C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\vcvarsall.bat" x64 && bash -c "make -C regression/cbmc test-paths-lifo BUILD_ENV=MSVC" '

buildspec.yml

@@ -26,7 +26,6 @@ phases:
       - make -C unit test
       - make -C regression test
       - make -C regression/cbmc test-paths-lifo
-      - scripts/delete_failing_smt2_solver_tests
       - env PATH=$PATH:`pwd`/src/solvers make -C regression/cbmc test-cprover-smt2
       - make -C jbmc/unit test
       - make -C jbmc/regression test

regression/cbmc/Anonymous_Struct3/test.desc

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

regression/cbmc/Array_operations1/test.desc

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

regression/cbmc/Bitfields3/paths.desc

@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 --pointer-check --bounds-check --paths lifo
 ^EXIT=0$

regression/cbmc/Bitfields3/test.desc

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

regression/cbmc/CMakeLists.txt

@@ -8,3 +8,15 @@ add_test_pl_profile(
     "-C;-X;thorough-paths;-X;smt-backend;-s;paths-lifo"
     "CORE"
 )
+
+add_test_pl_profile(
+    "cbmc-cprover-smt2"
+    "$<TARGET_FILE:cbmc> --cprover-smt2"
+    "-C;-X;broken-smt-backend;-s;cprover-smt2"
+    "CORE"
+)
+set_property(
+  TEST "cbmc-cprover-smt2-CORE"
+  PROPERTY ENVIRONMENT
+    "PATH=$ENV{PATH}:${CMAKE_BINARY_DIR}/bin"
+)

regression/cbmc/Empty_struct1/test.desc

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

regression/cbmc/Endianness4/test.desc

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

regression/cbmc/Endianness6/test.desc

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

regression/cbmc/Float-div2/test.desc

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

regression/cbmc/Float-div3/test.desc

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

regression/cbmc/Float-no-simp1/test.desc

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

regression/cbmc/Float-no-simp2/test.desc

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

regression/cbmc/Float-no-simp3/test.desc

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

regression/cbmc/Float-no-simp4/test.desc

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

regression/cbmc/Float-no-simp5/test.desc

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

regression/cbmc/Float-no-simp6/test.desc

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

regression/cbmc/Float-no-simp7/test.desc

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

regression/cbmc/Float-smt2-1/test.desc

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

regression/cbmc/Float-to-double2/test.desc

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

regression/cbmc/Float-to-int1/test.desc

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

regression/cbmc/Float-to-int2/test.desc

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

regression/cbmc/Float-to-int3/test.desc

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

regression/cbmc/Float-zero-sum1/test.desc

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

regression/cbmc/Float12/test.desc

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

regression/cbmc/Float13/test.desc

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

regression/cbmc/Float20/test.desc

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

regression/cbmc/Float22/test.desc

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

regression/cbmc/Float23/test.desc

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

regression/cbmc/Float3/test.desc

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

regression/cbmc/Float4/test.desc

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

regression/cbmc/Float5/test.desc

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

regression/cbmc/Float6/test.desc

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

regression/cbmc/Float8/test.desc

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

regression/cbmc/Linking4/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 link1.c
 link2.c
 ^EXIT=0$

regression/cbmc/Linking7/member-name-mismatch.desc

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

regression/cbmc/Linking7/test.desc

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

regression/cbmc/Makefile

@@ -4,7 +4,7 @@ test:
 	@../test.pl -p -c "../../../src/cbmc/cbmc --validate-goto-model" -X smt-backend
 
 test-cprover-smt2:
-	@../test.pl -p -c "../../../src/cbmc/cbmc --cprover-smt2"
+	@../test.pl -p -c "../../../src/cbmc/cbmc --cprover-smt2" -X broken-smt-backend
 
 test-paths-lifo:
 	@../test.pl -p -c "../../../src/cbmc/cbmc --paths lifo" -X thorough-paths -X smt-backend

regression/cbmc/Malloc23/test.desc

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

regression/cbmc/Multi_Dimensional_Array2/test.desc

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

regression/cbmc/Pointer_Arithmetic11/test.desc

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

regression/cbmc/Pointer_byte_extract2/test.desc

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

regression/cbmc/Pointer_byte_extract5/no-simplify.desc

@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.i
 --bounds-check --32 --no-simplify
 ^EXIT=10$

regression/cbmc/Pointer_byte_extract5/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.i
 --bounds-check --32
 ^EXIT=10$

regression/cbmc/Pointer_byte_extract9/test.desc

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

regression/cbmc/Promotion3/test.desc

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

regression/cbmc/Quantifiers-assertion/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 
 ^\*\* Results:$

regression/cbmc/Quantifiers-assignment/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 
 ^\*\* Results:$

regression/cbmc/Quantifiers-invalid-var-range/test.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+KNOWNBUG broken-smt-backend
 main.c
 
 ^\*\* Results:$

regression/cbmc/Quantifiers-type/test.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+KNOWNBUG broken-smt-backend
 main.c
 
 ^\*\* Results:$

regression/cbmc/Union_Initialization1/test.desc

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

regression/cbmc/address_space_size_limit1/test.desc

@@ -1,4 +1,4 @@
-CORE thorough-paths
+CORE thorough-paths broken-smt-backend
 test.c
 --no-simplify --unwind 300 --object-bits 8
 too many addressed objects

regression/cbmc/array-function-parameters/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 test.c
 --function test --min-null-tree-depth 2 --max-nondet-tree-depth 2 --bounds-check
 \[test.assertion.1\] line \d+ assertion Test.lists\[0\]->next: SUCCESS

regression/cbmc/array-tests/test.desc

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

regression/cbmc/bounds_check1/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 --bounds-check --pointer-check
 ^EXIT=10$

regression/cbmc/byte_update2/test.desc

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

regression/cbmc/byte_update3/test.desc

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

regression/cbmc/byte_update4/test.desc

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