Skip to content

Commit c4dccf4

Browse files
committed
Add --no-standard-checks to regression/cbmc-sequentialization test runner scripts
1 parent 2e4abb4 commit c4dccf4

File tree

2 files changed

+3
-3
lines changed

2 files changed

+3
-3
lines changed

Diff for: regression/cbmc-sequentialization/CMakeLists.txt

+2-2
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,10 @@
11
if(NOT WIN32)
22
add_test_pl_tests(
3-
"$<TARGET_FILE:cbmc> --validate-goto-model --validate-ssa-equation"
3+
"$<TARGET_FILE:cbmc> --no-standard-checks --validate-goto-model --validate-ssa-equation"
44
)
55
else()
66
add_test_pl_tests(
7-
"$<TARGET_FILE:cbmc> --validate-goto-model --validate-ssa-equation"
7+
"$<TARGET_FILE:cbmc> --no-standard-checks --validate-goto-model --validate-ssa-equation"
88
-X requires_posix_only_headers
99
)
1010
endif()

Diff for: regression/cbmc-sequentialization/Makefile

+1-1
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,7 @@ POSIX_ONLY =
1010
endif
1111

1212
test:
13-
@../test.pl -e -p -c "../../../src/cbmc/cbmc --validate-goto-model --validate-ssa-equation" $(POSIX_ONLY)
13+
@../test.pl -e -p -c "../../../src/cbmc/cbmc --no-standard-checks --validate-goto-model --validate-ssa-equation" $(POSIX_ONLY)
1414

1515
tests.log: ../test.pl test
1616

0 commit comments

Comments
 (0)