Skip to content

Commit 0d19437

Browse files
committed
Add --no-standard-checks to regression/goto-harness test runner script
1 parent 7d65934 commit 0d19437

File tree

1 file changed

+2
-0
lines changed

1 file changed

+2
-0
lines changed

regression/goto-harness/chain.sh

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -58,12 +58,14 @@ $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` \
6162
--pointer-check `# because we want to see out of bounds errors` \
6263
--unwind 11 `# with the way we set up arrays symex can't figure out loop bounds automatically` \
6364
--unwinding-assertions `# we want to make sure we don't accidentally pass tests because we didn't unwind enough` \
6465
# cbmc args end
6566
else
6667
$cbmc --function $entry_point "$input_c_file" "$harness_file" \
68+
--no-standard-checks `# deactivate default checks to make tests pass without significant adapting` \
6769
--pointer-check `# because we want to see out of bounds errors` \
6870
--unwind 11 `# with the way we set up arrays symex can't figure out loop bounds automatically` \
6971
--unwinding-assertions `# we want to make sure we don't accidentally pass tests because we didn't unwind enough` \

0 commit comments

Comments
 (0)