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

This will prevent the introduction of changes that violate the checks in the goto-validation procedure.
diffblue · Jan 28, 2019 · 933c2ef · 933c2ef
1 parent 1d40d38
commit 933c2ef
Show file tree

Hide file tree

Showing 3 changed files with 6 additions and 5 deletions.
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