Skip to content

Commit 20ee8df

Browse files
committed
Output goto functions in goto-harness regression tests
Adds two invocations of cbmc --show-goto-functions to regression/goto-harness/chain.sh to output the goto program before and after the harness generation.
1 parent 36983c1 commit 20ee8df

File tree

1 file changed

+2
-1
lines changed

1 file changed

+2
-1
lines changed

regression/goto-harness/chain.sh

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -24,8 +24,9 @@ if [ -e "${name}-mod.gb" ] ; then
2424
fi
2525

2626
# `# some comment` is an inline comment - basically, cause bash to execute an empty command
27-
27+
$cbmc --show-goto-functions "${name}.gb"
2828
$goto_harness "${name}.gb" "${name}-mod.gb" --harness-function-name $entry_point ${args}
29+
$cbmc --show-goto-functions "${name}-mod.gb"
2930
$cbmc --function $entry_point "${name}-mod.gb" \
3031
--pointer-check `# because we want to see out of bounds errors` \
3132
--unwind 11 `# with the way we set up arrays symex can't figure out loop bounds automatically` \

0 commit comments

Comments
 (0)