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

Daniel Kroening · chrisr-diffblue · commit a6b31234e6d5 · 2019-01-25T17:46:44.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/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/trace-values/trace-values.c b/regression/cbmc/trace-values/trace-values.c
@@ -1,3 +1,5 @@
+#include <stdlib.h>
+
 int global_var;
 
 struct S

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`	`)`