Run cbmc --full-slice in regression tests

To ensure --full-slice keeps working on all of CBMC's regression tests, run them in CI via an additional test profile. Some tests have to be excluded for they rely on program statements not being removed. Fixes: diffblue#260
tautschnig · Apr 11, 2022 · c1246c7 · c1246c7
1 parent 5ce50f5
commit c1246c7
Show file tree

Hide file tree

Showing 49 changed files with 57 additions and 94 deletions.
diff --git a/regression/cbmc/Bool5/full-slice.desc b/regression/cbmc/Bool5/full-slice.desc
diff --git a/regression/cbmc/CMakeLists.txt b/regression/cbmc/CMakeLists.txt
@@ -32,6 +32,13 @@ add_test_pl_profile(
   "CORE"
 )
 
+add_test_pl_profile(
+    "cbmc-full-slice"
+    "$<TARGET_FILE:cbmc> --validate-goto-model --validate-ssa-equation --full-slice"
+    "-C;-X;smt-backend;-X;broken-full-slice;-X;full-slice-expected-failure;${gcc_only_string}-s;full-slice"
+    "CORE"
+)
+
 # solver appears on the PATH in Windows already
 if(NOT "${CMAKE_SYSTEM_NAME}" STREQUAL "Windows")
   set_property(

diff --git a/regression/cbmc/Float24/test.desc b/regression/cbmc/Float24/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE full-slice-expected-failure
 main.i
 --win32 --xml-ui
 ^EXIT=10$

diff --git a/regression/cbmc/Makefile b/regression/cbmc/Makefile
@@ -34,6 +34,12 @@ test-new-smt-backend:
 					  -I new-smt-backend \
 					  -s new-smt-backend $(GCC_ONLY)
 
+test-full-slice:
+	@../test.pl -e -p -c "../../../src/cbmc/cbmc --validate-goto-model --validate-ssa-equation --full-slice" \
+		-X smt-backend $(GCC_ONLY) \
+		-X broken-full-slice -X full-slice-expected-failure
+		-s full-slice
+
 tests.log: ../test.pl test
 
 clean:

diff --git a/regression/cbmc/Pointer18/full-slice.desc b/regression/cbmc/Pointer18/full-slice.desc
diff --git a/regression/cbmc/array-cell-sensitivity1/test.desc b/regression/cbmc/array-cell-sensitivity1/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE full-slice-expected-failure
 test.c
 --show-vcc
 main::1::array!0@1#2\[\[1\]\] = main::1::array!0@1#1\[1\]

diff --git a/regression/cbmc/array-cell-sensitivity15/test.desc b/regression/cbmc/array-cell-sensitivity15/test.desc
@@ -1,4 +1,4 @@
-CORE paths-lifo-expected-failure
+CORE paths-lifo-expected-failure full-slice-expected-failure
 access.c
 --program-only
 ^EXIT=0$

diff --git a/regression/cbmc/array-cell-sensitivity2/test.desc b/regression/cbmc/array-cell-sensitivity2/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE full-slice-expected-failure
 test.c
 --show-vcc
 main::1::array!0@1#2 = with\(main::1::array!0@1#1, cast\(main::argc!0@1#1 \+ -1, signedbv\[64\]\), 1\)

diff --git a/regression/cbmc/array-cell-sensitivity9/test.desc b/regression/cbmc/array-cell-sensitivity9/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE full-slice-expected-failure
 test.c
 --show-vcc
 main::1::array!0@1#2\[\[0\]\]..x = main::1::array!0@1#1\[0\].x

diff --git a/regression/cbmc/array_of_bool_as_bitvec/test-smt2-outfile.desc b/regression/cbmc/array_of_bool_as_bitvec/test-smt2-outfile.desc
@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE broken-smt-backend full-slice-expected-failure
 main.c
 --smt2 --outfile -
 \(= \(select array_of\.2 i\) \(ite false #b1 #b0\)\)

diff --git a/regression/cbmc/byte-op-metric/test.desc b/regression/cbmc/byte-op-metric/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE full-slice-expected-failure
 main.c
 --show-byte-ops
 ^EXIT=0$

diff --git a/regression/cbmc/byte-op-metric/test_json.desc b/regression/cbmc/byte-op-metric/test_json.desc
@@ -1,4 +1,4 @@
-CORE
+CORE full-slice-expected-failure
 main.c
 --show-byte-ops --json-ui
 activate-multi-line-match

diff --git a/regression/cbmc/byte_update5/full-slice.desc b/regression/cbmc/byte_update5/full-slice.desc
diff --git a/regression/cbmc/compact-trace/test.desc b/regression/cbmc/compact-trace/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE full-slice-expected-failure
 main.c
 --compact-trace
 activate-multi-line-match

diff --git a/regression/cbmc/coverage_report1/paths.desc b/regression/cbmc/coverage_report1/paths.desc
@@ -1,4 +1,4 @@
-CORE
+CORE full-slice-expected-failure
 main.c
 --symex-coverage-report - --paths lifo
 <line branch="false" hits="1" number="12"/>

diff --git a/regression/cbmc/coverage_report1/test.desc b/regression/cbmc/coverage_report1/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE full-slice-expected-failure
 main.c
 --symex-coverage-report -
 <line branch="false" hits="1" number="12"/>

diff --git a/regression/cbmc/destructors/compound_literal.desc b/regression/cbmc/destructors/compound_literal.desc
@@ -1,4 +1,4 @@
-CORE
+CORE full-slice-expected-failure
 main.c
 --unwind 10 --show-goto-functions
 activate-multi-line-match

diff --git a/regression/cbmc/destructors/enter_lexical_block.desc b/regression/cbmc/destructors/enter_lexical_block.desc
@@ -1,4 +1,4 @@
-CORE
+CORE full-slice-expected-failure
 main.c
 --unwind 10 --show-goto-functions
 activate-multi-line-match

diff --git a/regression/cbmc/enum-trace1/test_json.desc b/regression/cbmc/enum-trace1/test_json.desc
@@ -1,4 +1,4 @@
-CORE
+CORE full-slice-expected-failure
 main.c
 --json-ui --function test --trace
 activate-multi-line-match

diff --git a/regression/cbmc/enum-trace1/test_xml.desc b/regression/cbmc/enum-trace1/test_xml.desc
@@ -1,4 +1,4 @@
-CORE
+CORE full-slice-expected-failure
 main.c
 --xml-ui --function test --trace
 activate-multi-line-match

diff --git a/regression/cbmc/field-sensitivity1/test.desc b/regression/cbmc/field-sensitivity1/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE full-slice-expected-failure
 test.c
 --show-vcc
 main::1::a!0@1#2\.\.x = main::argc!0@1#1

diff --git a/regression/cbmc/field-sensitivity10/test.desc b/regression/cbmc/field-sensitivity10/test.desc
@@ -1,8 +1,8 @@
 CORE
 test.c
 --show-vcc
-main::1::a1!0@1#2\.\.y =
-main::1::a2!0@1#2\.\.z =
+main::1::a1!0@1#[12]\.\.y =
+main::1::a2!0@1#[12]\.\.z =
 ^EXIT=0$
 ^SIGNAL=0$
 --

diff --git a/regression/cbmc/field-sensitivity2/test.desc b/regression/cbmc/field-sensitivity2/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE full-slice-expected-failure
 test.c
 --show-vcc
 main::1::a1!0@1#2\.\.x =

diff --git a/regression/cbmc/field-sensitivity3/test.desc b/regression/cbmc/field-sensitivity3/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE full-slice-expected-failure
 test.c
 --show-vcc
 main::1::a1!0@1#2\.\.x =

diff --git a/regression/cbmc/field-sensitivity8/test.desc b/regression/cbmc/field-sensitivity8/test.desc
@@ -1,8 +1,8 @@
 CORE
 test.c
 --show-vcc
-main::1::a1!0@1#2\.\.y =
-main::1::a2!0@1#2\.\.z =
+main::1::a1!0@1#[12]\.\.y =
+main::1::a2!0@1#[12]\.\.z =
 ^EXIT=0$
 ^SIGNAL=0$
 --

diff --git a/regression/cbmc/function-return-no-body1/test.desc b/regression/cbmc/function-return-no-body1/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE full-slice-expected-failure
 main.c
 --xml-ui
 activate-multi-line-match

diff --git a/regression/cbmc/graphml_witness1/test.desc b/regression/cbmc/graphml_witness1/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE full-slice-expected-failure
 main.c
 --graphml-witness -
 ^EXIT=10$

diff --git a/regression/cbmc/hex_trace/test.desc b/regression/cbmc/hex_trace/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE full-slice-expected-failure
 main.c
 --trace-hex --trace
 ^EXIT=10$

diff --git a/regression/cbmc/integer-assignments1/integer-typecheck.desc b/regression/cbmc/integer-assignments1/integer-typecheck.desc
@@ -1,4 +1,4 @@
-CORE
+CORE full-slice-expected-failure
 main.c
 --show-goto-functions
 ^[[:space:]]*ASSIGN main::1::b := main::1::b \* cast\(100, ℤ\)$

diff --git a/regression/cbmc/integer-assignments1/test.desc b/regression/cbmc/integer-assignments1/test.desc
@@ -1,4 +1,4 @@
-CORE smt-backend broken-smt-backend
+CORE smt-backend broken-smt-backend full-slice-expected-failure
 main.c
 --trace --smt2
 ^EXIT=10$

diff --git a/regression/cbmc/integral-trace/test.desc b/regression/cbmc/integral-trace/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE full-slice-expected-failure
 test.c
 --trace --xml-ui
 activate-multi-line-match

diff --git a/regression/cbmc/multiple-goto-traces/test.desc b/regression/cbmc/multiple-goto-traces/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE full-slice-expected-failure
 main.c
 --trace
 activate-multi-line-match

diff --git a/regression/cbmc/overflow/leftshift_overflow-c99-full-slice.desc b/regression/cbmc/overflow/leftshift_overflow-c99-full-slice.desc
diff --git a/regression/cbmc/printf1/test.desc b/regression/cbmc/printf1/test.desc
@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE broken-smt-backend full-slice-expected-failure
 main.c
 --trace
 ^EXIT=10$

diff --git a/regression/cbmc/reachability-slice-interproc/test.desc b/regression/cbmc/reachability-slice-interproc/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE full-slice-expected-failure
 test.c
 --reachability-slice-fb --show-goto-functions
 ^EXIT=0$

diff --git a/regression/cbmc/reachability-slice-interproc3/test.desc b/regression/cbmc/reachability-slice-interproc3/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE full-slice-expected-failure
 main.c
 --reachability-slice-fb --show-goto-functions
 ^EXIT=0$

diff --git a/regression/cbmc/reachability-slice/test.desc b/regression/cbmc/reachability-slice/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE full-slice-expected-failure
 test.c
 --reachability-slice --show-goto-functions --cover location --property foo.coverage.2
 ^EXIT=0$

diff --git a/regression/cbmc/reachability-slice/test2.desc b/regression/cbmc/reachability-slice/test2.desc
@@ -1,4 +1,4 @@
-CORE
+CORE full-slice-expected-failure
 test.c
 --reachability-slice-fb --show-goto-functions --cover location --property foo.coverage.2
 ^EXIT=0$

diff --git a/regression/cbmc/reachability-slice/test3.desc b/regression/cbmc/reachability-slice/test3.desc
@@ -1,4 +1,4 @@
-CORE
+CORE full-slice-expected-failure
 test.c
 --reachability-slice --show-goto-functions --cover location
 ^EXIT=0$

diff --git a/regression/cbmc/return3/full-slice.desc b/regression/cbmc/return3/full-slice.desc
diff --git a/regression/cbmc/show-vcc/main_prec.desc b/regression/cbmc/show-vcc/main_prec.desc
@@ -1,4 +1,4 @@
-CORE
+CORE full-slice-expected-failure
 main_prec.c
 --show-vcc
 ^EXIT=0$

diff --git a/regression/cbmc/show-vcc/test.desc b/regression/cbmc/show-vcc/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE full-slice-expected-failure
 main.c
 --show-vcc
 ^EXIT=0$

diff --git a/regression/cbmc/symex_should_evaluate_simple_pointer_conditions/test.desc b/regression/cbmc/symex_should_evaluate_simple_pointer_conditions/test.desc
@@ -1,4 +1,4 @@
-CORE paths-lifo-expected-failure
+CORE paths-lifo-expected-failure full-slice-expected-failure
 test.c
 --function test --show-vcc
 ^EXIT=0$

diff --git a/regression/cbmc/symex_should_exclude_null_pointers/test.desc b/regression/cbmc/symex_should_exclude_null_pointers/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE full-slice-expected-failure
 main.c
 --show-vcc
 ^EXIT=0$

diff --git a/regression/cbmc/symex_should_filter_value_sets/test.desc b/regression/cbmc/symex_should_filter_value_sets/test.desc
@@ -1,4 +1,4 @@
-CORE paths-lifo-expected-failure
+CORE paths-lifo-expected-failure full-slice-expected-failure
 main.c
 --show-vcc
 ^EXIT=0$

diff --git a/regression/cbmc/trace-strings/test.desc b/regression/cbmc/trace-strings/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE full-slice-expected-failure
 main.c
 --trace
 ^EXIT=10$

diff --git a/regression/cbmc/trace-values/trace-values.desc b/regression/cbmc/trace-values/trace-values.desc
@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE broken-smt-backend full-slice-expected-failure
 trace-values.c
 --trace
 ^EXIT=10$

diff --git a/regression/cbmc/trace_address_arithmetic1/test.desc b/regression/cbmc/trace_address_arithmetic1/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE full-slice-expected-failure
 main.c
 --trace
 ^EXIT=10$

diff --git a/regression/cbmc/trace_show_code/test.desc b/regression/cbmc/trace_show_code/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE full-slice-expected-failure
 main.c
 --trace --trace-show-code
 ^EXIT=10$