Run cbmc --full-slice in regression tests

tautschnig · tautschnig · commit c1246c797905 · 2022-04-11T20:03:08.000Z
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
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$

Original file line number	Diff line number	Diff line change
`@@ -1,4 +1,4 @@`
`1`		`-CORE`
	`1`	`+CORE full-slice-expected-failure`
`2`	`2`	`main.i`
`3`	`3`	`--win32 --xml-ui`
`4`	`4`	`^EXIT=10$`
Original file line number	Diff line number	Diff line change
`@@ -1,4 +1,4 @@`
`1`		`-CORE paths-lifo-expected-failure`
	`1`	`+CORE paths-lifo-expected-failure full-slice-expected-failure`
`2`	`2`	`access.c`
`3`	`3`	`--program-only`
`4`	`4`	`^EXIT=0$`
Original file line number	Diff line number	Diff line change
`@@ -1,4 +1,4 @@`
`1`		`-CORE broken-smt-backend`
	`1`	`+CORE broken-smt-backend full-slice-expected-failure`
`2`	`2`	`main.c`
`3`	`3`	`--smt2 --outfile -`
`4`	`4`	`\(= \(select array_of\.2 i\) \(ite false #b1 #b0\)\)`
Original file line number	Diff line number	Diff line change
`@@ -1,4 +1,4 @@`
`1`		`-CORE smt-backend broken-smt-backend`
	`1`	`+CORE smt-backend broken-smt-backend full-slice-expected-failure`
`2`	`2`	`main.c`
`3`	`3`	`--trace --smt2`
`4`	`4`	`^EXIT=10$`