Skip to content

Commit 9ede58f

Browse files
committed
Add --no-malloc-fail to test runners
In order to keep existing tests passing.
1 parent ba28aa5 commit 9ede58f

File tree

3 files changed

+6
-6
lines changed

3 files changed

+6
-6
lines changed

regression/contracts-dfcc/chain.sh

+1-1
Original file line numberDiff line numberDiff line change
@@ -58,5 +58,5 @@ elif echo $args_inst | grep -q -- "--dump-c" ; then
5858

5959
rm "${name}${dfcc_suffix}-mod.c"
6060
fi
61-
$goto_instrument --show-goto-functions "${name}${dfcc_suffix}-mod.gb"
61+
$goto_instrument --no-malloc-fail --show-goto-functions "${name}${dfcc_suffix}-mod.gb"
6262
$cbmc --no-standard-checks "${name}${dfcc_suffix}-mod.gb" ${args_cbmc}

regression/goto-instrument/chain.sh

+2-2
Original file line numberDiff line numberDiff line change
@@ -21,7 +21,7 @@ else
2121
fi
2222

2323
rm -f "${target}-mod.gb"
24-
$goto_instrument ${args} "${target}.gb" "${target}-mod.gb"
24+
$goto_instrument --no-malloc-fail ${args} "${target}.gb" "${target}-mod.gb"
2525
if [ ! -e "${target}-mod.gb" ] ; then
2626
cp "${target}.gb" "${target}-mod.gb"
2727
elif echo $args | grep -q -- "--dump-c-type-header" ; then
@@ -39,5 +39,5 @@ elif echo $args | grep -q -- "--dump-c" ; then
3939

4040
rm "${target}-mod.c"
4141
fi
42-
$goto_instrument --show-goto-functions "${target}-mod.gb"
42+
$goto_instrument --no-malloc-fail --show-goto-functions "${target}-mod.gb"
4343
$cbmc --no-standard-checks "${target}-mod.gb"

regression/goto-synthesizer/chain.sh

+3-3
Original file line numberDiff line numberDiff line change
@@ -37,7 +37,7 @@ fi
3737
rm -f "${name}-mod.gb"
3838
rm -f "${name}-mod-2.gb"
3939
echo "Running goto-instrument: "
40-
$goto_instrument ${args_inst} "${name}.gb" "${name}-mod.gb"
40+
$goto_instrument --no-malloc-fail ${args_inst} "${name}.gb" "${name}-mod.gb"
4141
if [ ! -e "${name}-mod.gb" ] ; then
4242
cp "$name.gb" "${name}-mod.gb"
4343
elif echo $args_inst | grep -q -- "--dump-c" ; then
@@ -53,9 +53,9 @@ elif echo $args_inst | grep -q -- "--dump-c" ; then
5353
fi
5454
echo "Running goto-synthesizer: "
5555
if echo $args_synthesizer | grep -q -- "--dump-loop-contracts" ; then
56-
$goto_synthesizer ${args_synthesizer} "${name}-mod.gb"
56+
$goto_synthesizer ${args_synthesizer} --no-malloc-fail "${name}-mod.gb"
5757
else
58-
$goto_synthesizer ${args_synthesizer} "${name}-mod.gb" "${name}-mod-2.gb"
58+
$goto_synthesizer ${args_synthesizer} --no-malloc-fail "${name}-mod.gb" "${name}-mod-2.gb"
5959
echo "Running CBMC: "
6060
$cbmc --no-standard-checks ${args_cbmc} "${name}-mod-2.gb"
6161
fi

0 commit comments

Comments
 (0)