Skip to content

Commit c3c7bc0

Browse files
author
Enrico Steffinlongo
committed
Renamed no-malloc-fail to no-malloc-may-fail to mirror malloc-may-fail on tests runners
1 parent c63610b commit c3c7bc0

File tree

3 files changed

+6
-6
lines changed

3 files changed

+6
-6
lines changed

Diff for: regression/contracts-dfcc/chain.sh

+1-1
Original file line numberDiff line numberDiff line change
@@ -44,7 +44,7 @@ else
4444
fi
4545

4646
if [[ "${args_inst}" != *"malloc"* ]]; then
47-
args_inst="--no-malloc-fail $args_inst"
47+
args_inst="--no-malloc-may-fail $args_inst"
4848
fi
4949

5050
rm -f "${name}${dfcc_suffix}-mod.gb"

Diff for: 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 --no-malloc-fail ${args} "${target}.gb" "${target}-mod.gb"
24+
$goto_instrument --no-malloc-may-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 --no-malloc-fail --show-goto-functions "${target}-mod.gb"
42+
$goto_instrument --no-malloc-may-fail --show-goto-functions "${target}-mod.gb"
4343
$cbmc --no-standard-checks "${target}-mod.gb"

Diff for: 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 --no-malloc-fail ${args_inst} "${name}.gb" "${name}-mod.gb"
40+
$goto_instrument --no-malloc-may-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} --no-malloc-fail "${name}-mod.gb"
56+
$goto_synthesizer ${args_synthesizer} --no-malloc-may-fail "${name}-mod.gb"
5757
else
58-
$goto_synthesizer ${args_synthesizer} --no-malloc-fail "${name}-mod.gb" "${name}-mod-2.gb"
58+
$goto_synthesizer ${args_synthesizer} --no-malloc-may-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)