Merge pull request #4121 from tautschnig/smt-solver-cmake-tests

tautschnig · web-flow · commit f4ed82aa8e62 · 2019-02-14T07:08:52.000Z
Cleanup of SMT2 solver test execution and CMake support [blocks: #4063]
diff --git a/.travis.yml b/.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
diff --git a/CODEOWNERS b/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
diff --git a/buildspec-linux-clang.yml b/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
diff --git a/buildspec-windows.yml b/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" '
diff --git a/buildspec.yml b/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
diff --git a/regression/cbmc/Anonymous_Struct3/test.desc b/regression/cbmc/Anonymous_Struct3/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/Array_operations1/test.desc b/regression/cbmc/Array_operations1/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 
 ^EXIT=10$
diff --git a/regression/cbmc/Bitfields3/paths.desc b/regression/cbmc/Bitfields3/paths.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 --pointer-check --bounds-check --paths lifo
 ^EXIT=0$
diff --git a/regression/cbmc/Bitfields3/test.desc b/regression/cbmc/Bitfields3/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 --pointer-check --bounds-check
 ^EXIT=0$
diff --git a/regression/cbmc/CMakeLists.txt b/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"
+)
diff --git a/regression/cbmc/Empty_struct1/test.desc b/regression/cbmc/Empty_struct1/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/Endianness4/test.desc b/regression/cbmc/Endianness4/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/Endianness6/test.desc b/regression/cbmc/Endianness6/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 --big-endian
 ^EXIT=0$
diff --git a/regression/cbmc/Float-div2/test.desc b/regression/cbmc/Float-div2/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 --floatbv
 ^EXIT=0$
diff --git a/regression/cbmc/Float-div3/test.desc b/regression/cbmc/Float-div3/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 --floatbv
 ^EXIT=0$
diff --git a/regression/cbmc/Float-no-simp1/test.desc b/regression/cbmc/Float-no-simp1/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 --no-simplify
 ^EXIT=0$
diff --git a/regression/cbmc/Float-no-simp2/test.desc b/regression/cbmc/Float-no-simp2/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 --floatbv --no-simplify
 ^EXIT=0$
diff --git a/regression/cbmc/Float-no-simp3/test.desc b/regression/cbmc/Float-no-simp3/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 --floatbv --no-simplify
 ^EXIT=0$
diff --git a/regression/cbmc/Float-no-simp4/test.desc b/regression/cbmc/Float-no-simp4/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 --floatbv --no-simplify
 ^EXIT=0$
diff --git a/regression/cbmc/Float-no-simp5/test.desc b/regression/cbmc/Float-no-simp5/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 --floatbv --no-simplify
 ^EXIT=0$
diff --git a/regression/cbmc/Float-no-simp6/test.desc b/regression/cbmc/Float-no-simp6/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 --floatbv --no-simplify
 ^EXIT=0$
diff --git a/regression/cbmc/Float-no-simp7/test.desc b/regression/cbmc/Float-no-simp7/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 --floatbv --no-simplify
 ^EXIT=0$
diff --git a/regression/cbmc/Float-smt2-1/test.desc b/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$
diff --git a/regression/cbmc/Float-to-double2/test.desc b/regression/cbmc/Float-to-double2/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 --floatbv --no-simplify
 ^EXIT=0$
diff --git a/regression/cbmc/Float-to-int1/test.desc b/regression/cbmc/Float-to-int1/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 --floatbv
 ^EXIT=0$
diff --git a/regression/cbmc/Float-to-int2/test.desc b/regression/cbmc/Float-to-int2/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 --floatbv
 ^EXIT=0$
diff --git a/regression/cbmc/Float-to-int3/test.desc b/regression/cbmc/Float-to-int3/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 --floatbv
 ^EXIT=0$
diff --git a/regression/cbmc/Float-zero-sum1/test.desc b/regression/cbmc/Float-zero-sum1/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 --floatbv --no-simplify
 ^EXIT=0$
diff --git a/regression/cbmc/Float12/test.desc b/regression/cbmc/Float12/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/Float13/test.desc b/regression/cbmc/Float13/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/Float20/test.desc b/regression/cbmc/Float20/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 --floatbv
 ^EXIT=0$
diff --git a/regression/cbmc/Float22/test.desc b/regression/cbmc/Float22/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 --floatbv
 ^EXIT=0$
diff --git a/regression/cbmc/Float23/test.desc b/regression/cbmc/Float23/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/Float3/test.desc b/regression/cbmc/Float3/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 --floatbv
 ^EXIT=0$
diff --git a/regression/cbmc/Float4/test.desc b/regression/cbmc/Float4/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 --floatbv
 ^EXIT=0$
diff --git a/regression/cbmc/Float5/test.desc b/regression/cbmc/Float5/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 --floatbv
 ^EXIT=0$
diff --git a/regression/cbmc/Float6/test.desc b/regression/cbmc/Float6/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 --floatbv
 ^EXIT=0$
diff --git a/regression/cbmc/Float8/test.desc b/regression/cbmc/Float8/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/Linking4/test.desc b/regression/cbmc/Linking4/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 link1.c
 link2.c
 ^EXIT=0$
diff --git a/regression/cbmc/Linking7/member-name-mismatch.desc b/regression/cbmc/Linking7/member-name-mismatch.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 module2.c
 ^EXIT=10$
diff --git a/regression/cbmc/Linking7/test.desc b/regression/cbmc/Linking7/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 module.c
 ^EXIT=10$
diff --git a/regression/cbmc/Makefile b/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
diff --git a/regression/cbmc/Malloc23/test.desc b/regression/cbmc/Malloc23/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 --pointer-check
 ^EXIT=10$
diff --git a/regression/cbmc/Multi_Dimensional_Array2/test.desc b/regression/cbmc/Multi_Dimensional_Array2/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/Pointer_Arithmetic11/test.desc b/regression/cbmc/Pointer_Arithmetic11/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 --pointer-check --little-endian
 ^EXIT=0$
diff --git a/regression/cbmc/Pointer_byte_extract2/test.desc b/regression/cbmc/Pointer_byte_extract2/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 --little-endian
 ^EXIT=10$
diff --git a/regression/cbmc/Pointer_byte_extract5/no-simplify.desc b/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$
diff --git a/regression/cbmc/Pointer_byte_extract5/test.desc b/regression/cbmc/Pointer_byte_extract5/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.i
 --bounds-check --32
 ^EXIT=10$
diff --git a/regression/cbmc/Pointer_byte_extract9/test.desc b/regression/cbmc/Pointer_byte_extract9/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 
 ^EXIT=10$
diff --git a/regression/cbmc/Promotion3/test.desc b/regression/cbmc/Promotion3/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/Quantifiers-assertion/test.desc b/regression/cbmc/Quantifiers-assertion/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 
 ^\*\* Results:$
diff --git a/regression/cbmc/Quantifiers-assignment/test.desc b/regression/cbmc/Quantifiers-assignment/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 
 ^\*\* Results:$
diff --git a/regression/cbmc/Quantifiers-invalid-var-range/test.desc b/regression/cbmc/Quantifiers-invalid-var-range/test.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+KNOWNBUG broken-smt-backend
 main.c
 
 ^\*\* Results:$
diff --git a/regression/cbmc/Quantifiers-type/test.desc b/regression/cbmc/Quantifiers-type/test.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+KNOWNBUG broken-smt-backend
 main.c
 
 ^\*\* Results:$
diff --git a/regression/cbmc/Union_Initialization1/test.desc b/regression/cbmc/Union_Initialization1/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/address_space_size_limit1/test.desc b/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
diff --git a/regression/cbmc/array-function-parameters/test.desc b/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
diff --git a/regression/cbmc/array-tests/test.desc b/regression/cbmc/array-tests/test.desc
@@ -1,4 +1,4 @@
-CORE thorough-paths
+CORE thorough-paths broken-smt-backend
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/bounds_check1/test.desc b/regression/cbmc/bounds_check1/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 --bounds-check --pointer-check
 ^EXIT=10$
diff --git a/regression/cbmc/byte_update2/test.desc b/regression/cbmc/byte_update2/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 --little-endian
 ^EXIT=0$
diff --git a/regression/cbmc/byte_update3/test.desc b/regression/cbmc/byte_update3/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 --little-endian
 ^EXIT=0$
diff --git a/regression/cbmc/byte_update4/test.desc b/regression/cbmc/byte_update4/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 --little-endian
 ^EXIT=0$
diff --git a/regression/cbmc/byte_update5/test.desc b/regression/cbmc/byte_update5/test.desc
diff --git a/regression/cbmc/byte_update6/test.desc b/regression/cbmc/byte_update6/test.desc
diff --git a/regression/cbmc/byte_update7/test.desc b/regression/cbmc/byte_update7/test.desc
diff --git a/regression/cbmc/byte_update8/test.desc b/regression/cbmc/byte_update8/test.desc
diff --git a/regression/cbmc/byte_update9/test.desc b/regression/cbmc/byte_update9/test.desc
diff --git a/regression/cbmc/compact-trace/test.desc b/regression/cbmc/compact-trace/test.desc
diff --git a/regression/cbmc/dynamic_size1/stack_object.desc b/regression/cbmc/dynamic_size1/stack_object.desc
diff --git a/regression/cbmc/graphml_witness1/test.desc b/regression/cbmc/graphml_witness1/test.desc
diff --git a/regression/cbmc/integer-assignments1/test.desc b/regression/cbmc/integer-assignments1/test.desc
diff --git a/regression/cbmc/memory_allocation1/test.desc b/regression/cbmc/memory_allocation1/test.desc
diff --git a/regression/cbmc/pointer-function-parameters-struct-mutual-recursion/test.desc b/regression/cbmc/pointer-function-parameters-struct-mutual-recursion/test.desc
diff --git a/regression/cbmc/pointer-function-parameters-struct-simple-recursion-2/test.desc b/regression/cbmc/pointer-function-parameters-struct-simple-recursion-2/test.desc
diff --git a/regression/cbmc/pointer-function-parameters-struct-simple-recursion/test.desc b/regression/cbmc/pointer-function-parameters-struct-simple-recursion/test.desc
diff --git a/regression/cbmc/scanf1/test.desc b/regression/cbmc/scanf1/test.desc
diff --git a/regression/cbmc/stack-trace/test.desc b/regression/cbmc/stack-trace/test.desc
diff --git a/regression/cbmc/struct6/test.desc b/regression/cbmc/struct6/test.desc
diff --git a/regression/cbmc/struct7/test.desc b/regression/cbmc/struct7/test.desc
diff --git a/regression/cbmc/trace-values/trace-values.desc b/regression/cbmc/trace-values/trace-values.desc
diff --git a/regression/cbmc/trace_show_function_calls/test.desc b/regression/cbmc/trace_show_function_calls/test.desc
diff --git a/regression/cbmc/uninterpreted_function/uf1.desc b/regression/cbmc/uninterpreted_function/uf1.desc
diff --git a/regression/cbmc/uninterpreted_function/uf2.desc b/regression/cbmc/uninterpreted_function/uf2.desc
diff --git a/regression/cbmc/union12/test.desc b/regression/cbmc/union12/test.desc
diff --git a/regression/cbmc/union6/test.desc b/regression/cbmc/union6/test.desc
diff --git a/regression/cbmc/union7/test.desc b/regression/cbmc/union7/test.desc
diff --git a/regression/cbmc/union9/test.desc b/regression/cbmc/union9/test.desc
diff --git a/regression/cbmc/variable-access-to-constant-array/test.desc b/regression/cbmc/variable-access-to-constant-array/test.desc
diff --git a/regression/cbmc/void_pointer2/test.desc b/regression/cbmc/void_pointer2/test.desc
diff --git a/regression/cbmc/void_pointer3/test.desc b/regression/cbmc/void_pointer3/test.desc
diff --git a/regression/cbmc/void_pointer4/test.desc b/regression/cbmc/void_pointer4/test.desc
diff --git a/scripts/delete_failing_smt2_solver_tests b/scripts/delete_failing_smt2_solver_tests

Original file line number	Diff line number	Diff line change
`@@ -1,4 +1,4 @@`
`1`		`-CORE`
	`1`	`+CORE broken-smt-backend`
`2`	`2`	`main.c`
`3`	`3`
`4`	`4`	`^EXIT=0$`
Original file line number	Diff line number	Diff line change
`@@ -1,4 +1,4 @@`
`1`		`-CORE smt-backend`
	`1`	`+CORE smt-backend broken-smt-backend`
`2`	`2`	`main.c`
`3`	`3`	`--smt2`
`4`	`4`	`^EXIT=10$`
Original file line number	Diff line number	Diff line change
`@@ -1,4 +1,4 @@`
`1`		`-KNOWNBUG`
	`1`	`+KNOWNBUG broken-smt-backend`
`2`	`2`	`main.c`
`3`	`3`
`4`	`4`	`^\\ Results:$`
Original file line number	Diff line number	Diff line change
`@@ -1,4 +1,4 @@`
`1`		`-CORE thorough-paths`
	`1`	`+CORE thorough-paths broken-smt-backend`
`2`	`2`	`test.c`
`3`	`3`	`--no-simplify --unwind 300 --object-bits 8`
`4`	`4`	`too many addressed objects`