Skip to content

Commit 51a0429

Browse files
committed
Revert "Add --no-standard-checks to regression/goto-harness test runner script"
This reverts commit 0d19437.
1 parent a225e12 commit 51a0429

File tree

1 file changed

+0
-2
lines changed

1 file changed

+0
-2
lines changed

regression/goto-harness/chain.sh

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -58,14 +58,12 @@ $goto_harness "$input_goto_binary" "$harness_file" --harness-function-name $entr
5858
$cbmc --show-goto-functions "$harness_file"
5959
if [[ "${harness_file}" == "harness.gb" ]];then
6060
$cbmc --function $entry_point "$harness_file" \
61-
--no-standard-checks `# deactivate default checks to make tests pass without significant adapting` \
6261
--pointer-check `# because we want to see out of bounds errors` \
6362
--unwind 11 `# with the way we set up arrays symex can't figure out loop bounds automatically` \
6463
--unwinding-assertions `# we want to make sure we don't accidentally pass tests because we didn't unwind enough` \
6564
# cbmc args end
6665
else
6766
$cbmc --function $entry_point "$input_c_file" "$harness_file" \
68-
--no-standard-checks `# deactivate default checks to make tests pass without significant adapting` \
6967
--pointer-check `# because we want to see out of bounds errors` \
7068
--unwind 11 `# with the way we set up arrays symex can't figure out loop bounds automatically` \
7169
--unwinding-assertions `# we want to make sure we don't accidentally pass tests because we didn't unwind enough` \

0 commit comments

Comments
 (0)