enable --validate-goto-model for all cbmc regressions

kroening · kroening · commit 6e46bca6e6b9 · 2019-01-03T20:41:53.000Z
This will prevent the introduction of changes that violate the checks
in the goto-validation procedure.
diff --git a/regression/cbmc/CMakeLists.txt b/regression/cbmc/CMakeLists.txt
@@ -1,3 +1,3 @@
 add_test_pl_tests(
-    "$<TARGET_FILE:cbmc>" -X smt-backend
+    "$<TARGET_FILE:cbmc> --validate-goto-model" -X smt-backend
 )
diff --git a/regression/cbmc/Float-zero-sum1/test.desc b/regression/cbmc/Float-zero-sum1/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --floatbv --no-simplify
 ^EXIT=0$
diff --git a/regression/cbmc/Float22/test.desc b/regression/cbmc/Float22/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --floatbv
 ^EXIT=0$
diff --git a/regression/cbmc/Function10/test.desc b/regression/cbmc/Function10/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/Function12/test.desc b/regression/cbmc/Function12/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/Function_Pointer10/test.desc b/regression/cbmc/Function_Pointer10/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/Function_Pointer11/test.desc b/regression/cbmc/Function_Pointer11/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/Function_Pointer8/test.desc b/regression/cbmc/Function_Pointer8/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 
 ^EXIT=10$
diff --git a/regression/cbmc/Global_Initialization2/test.desc b/regression/cbmc/Global_Initialization2/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/Linking7/return_type.desc b/regression/cbmc/Linking7/return_type.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 return_type1.c
 return_type2.c
 ^EXIT=0$
diff --git a/regression/cbmc/Makefile b/regression/cbmc/Makefile
@@ -1,13 +1,12 @@
-default: tests.log
+default: test
 
 test:
-	@../test.pl -p -c ../../../src/cbmc/cbmc -X smt-backend
+	@../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"
 
-tests.log: ../test.pl
-	@../test.pl -p -c ../../../src/cbmc/cbmc -X smt-backend
+tests.log: ../test.pl test
 
 show:
 	@for dir in *; do \
diff --git a/regression/cbmc/Malloc16/test.desc b/regression/cbmc/Malloc16/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.i
 --32
 ^EXIT=0$
diff --git a/regression/cbmc/Zero_Initialization1/test.desc b/regression/cbmc/Zero_Initialization1/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/array-function-parameters/test.desc b/regression/cbmc/array-function-parameters/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 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/atomic_section_seq1/test.desc b/regression/cbmc/atomic_section_seq1/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 
 ^EXIT=10$
diff --git a/regression/cbmc/compact-trace/test.desc b/regression/cbmc/compact-trace/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --compact-trace
 activate-multi-line-match
diff --git a/regression/cbmc/constructor1/test.desc b/regression/cbmc/constructor1/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/enum1/test.desc b/regression/cbmc/enum1/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/enum2/test.desc b/regression/cbmc/enum2/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/gcc_statement_expression3/test.desc b/regression/cbmc/gcc_statement_expression3/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/memset1/test.desc b/regression/cbmc/memset1/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 
 ^EXIT=10$
diff --git a/regression/cbmc/memset2/test.desc b/regression/cbmc/memset2/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/memset3/test.desc b/regression/cbmc/memset3/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --pointer-check
 ^EXIT=10$
diff --git a/regression/cbmc/noop1/test.desc b/regression/cbmc/noop1/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/path-branch-pointer-call/test.desc b/regression/cbmc/path-branch-pointer-call/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --paths lifo
 ^EXIT=0$
diff --git a/regression/cbmc/pointer-function-parameters-struct-mutual-recursion/test.desc b/regression/cbmc/pointer-function-parameters-struct-mutual-recursion/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --function func --min-null-tree-depth 10 --max-nondet-tree-depth 3 --pointer-check
 ^EXIT=0$
diff --git a/regression/cbmc/pointer-function-parameters-struct-non-recursive/test.desc b/regression/cbmc/pointer-function-parameters-struct-non-recursive/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --function func --min-null-tree-depth 10
 ^EXIT=10$
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
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --function func --min-null-tree-depth 10 --max-nondet-tree-depth 2 --pointer-check
 ^EXIT=0$
diff --git a/regression/cbmc/pointer-function-parameters-struct-simple-recursion-3/test.desc b/regression/cbmc/pointer-function-parameters-struct-simple-recursion-3/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --function func --min-null-tree-depth 2 --max-nondet-tree-depth 10 --cover branch
 ^EXIT=0$
diff --git a/regression/cbmc/pointer-function-parameters-struct-simple-recursion/test.desc b/regression/cbmc/pointer-function-parameters-struct-simple-recursion/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --function func --min-null-tree-depth 10 --max-nondet-tree-depth 3 --pointer-check
 ^EXIT=0$
diff --git a/regression/cbmc/reachability-slice-interproc2/test.desc b/regression/cbmc/reachability-slice-interproc2/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --reachability-slice --show-goto-functions
 ^EXIT=0$
diff --git a/regression/cbmc/return1/test.desc b/regression/cbmc/return1/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/show_properties1/test.desc b/regression/cbmc/show_properties1/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --pointer-check --show-properties
 ^EXIT=0$
diff --git a/regression/cbmc/simplify-full-test/test.desc b/regression/cbmc/simplify-full-test/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/simplify-function-call-array-element-pointer/test.desc b/regression/cbmc/simplify-function-call-array-element-pointer/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/simplify-function-call-array-pointer/test.desc b/regression/cbmc/simplify-function-call-array-pointer/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/simplify-function-call-pointer-access/test.desc b/regression/cbmc/simplify-function-call-pointer-access/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/stack-trace/test.desc b/regression/cbmc/stack-trace/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --stack-trace
 activate-multi-line-match
diff --git a/regression/cbmc/trace-values/trace-values.desc b/regression/cbmc/trace-values/trace-values.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 trace-values.c
 --trace
 ^EXIT=10$
diff --git a/regression/cbmc/typedef-param-anon-union1/test.desc b/regression/cbmc/typedef-param-anon-union1/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --show-symbol-table --function fun
 // Enable multi-line checking
diff --git a/regression/cbmc/typedef-param-union1/test.desc b/regression/cbmc/typedef-param-union1/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --show-symbol-table --function fun
 // Enable multi-line checking

Original file line number	Diff line number	Diff line change
`@@ -1,3 +1,3 @@`
`1`	`1`	`add_test_pl_tests(`
`2`		`- "$<TARGET_FILE:cbmc>" -X smt-backend`
	`2`	`+ "$<TARGET_FILE:cbmc> --validate-goto-model" -X smt-backend`
`3`	`3`	`)`
Original file line number	Diff line number	Diff line change
`@@ -1,4 +1,4 @@`
`1`		`-CORE`
	`1`	`+KNOWNBUG`
`2`	`2`	`main.c`
`3`	`3`	`--floatbv --no-simplify`
`4`	`4`	`^EXIT=0$`