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

Daniel Kroening · Daniel Kroening · commit 74722af75e5f · 2019-01-03T17:28: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/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 \

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