Skip to content

Commit c1bfa90

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 81ad86d commit c1bfa90

File tree

1 file changed

+3
-1
lines changed

1 file changed

+3
-1
lines changed

regression/goto-harness/chain.sh

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -23,5 +23,7 @@ if [ -e "${name}-mod.gb" ] ; then
2323
rm -f "${name}-mod.gb"
2424
fi
2525

26-
$goto_harness "${name}.gb" "${name}-mod.gb" --harness-function-name $entry_point ${args}
26+
$cbmc --show-goto-functions "${name}.gb"
27+
$goto_harness "${name}.gb" "${name}-mod.gb" --harness-function-name $entry_point ${args}
28+
$cbmc --show-goto-functions "${name}-mod.gb"
2729
$cbmc --function $entry_point "${name}-mod.gb"

0 commit comments

Comments
 (0)