diff --git a/regression/contracts-dfcc/chain.sh b/regression/contracts-dfcc/chain.sh index 0d61c8b1f38..8b931718943 100755 --- a/regression/contracts-dfcc/chain.sh +++ b/regression/contracts-dfcc/chain.sh @@ -44,7 +44,7 @@ else fi if [[ "${args_inst}" != *"malloc"* ]]; then - args_inst="--no-malloc-fail $args_inst" + args_inst="--no-malloc-may-fail $args_inst" fi rm -f "${name}${dfcc_suffix}-mod.gb" diff --git a/regression/goto-instrument/chain.sh b/regression/goto-instrument/chain.sh index 7f596e9f0fb..96ebce32760 100755 --- a/regression/goto-instrument/chain.sh +++ b/regression/goto-instrument/chain.sh @@ -21,7 +21,7 @@ else fi rm -f "${target}-mod.gb" -$goto_instrument --no-malloc-fail ${args} "${target}.gb" "${target}-mod.gb" +$goto_instrument --no-malloc-may-fail ${args} "${target}.gb" "${target}-mod.gb" if [ ! -e "${target}-mod.gb" ] ; then cp "${target}.gb" "${target}-mod.gb" elif echo $args | grep -q -- "--dump-c-type-header" ; then @@ -39,5 +39,5 @@ elif echo $args | grep -q -- "--dump-c" ; then rm "${target}-mod.c" fi -$goto_instrument --no-malloc-fail --show-goto-functions "${target}-mod.gb" +$goto_instrument --no-malloc-may-fail --show-goto-functions "${target}-mod.gb" $cbmc --no-standard-checks "${target}-mod.gb" diff --git a/regression/goto-synthesizer/chain.sh b/regression/goto-synthesizer/chain.sh index 50e1b6240ff..d6379cac470 100755 --- a/regression/goto-synthesizer/chain.sh +++ b/regression/goto-synthesizer/chain.sh @@ -37,7 +37,7 @@ fi rm -f "${name}-mod.gb" rm -f "${name}-mod-2.gb" echo "Running goto-instrument: " -$goto_instrument --no-malloc-fail ${args_inst} "${name}.gb" "${name}-mod.gb" +$goto_instrument --no-malloc-may-fail ${args_inst} "${name}.gb" "${name}-mod.gb" if [ ! -e "${name}-mod.gb" ] ; then cp "$name.gb" "${name}-mod.gb" elif echo $args_inst | grep -q -- "--dump-c" ; then @@ -53,9 +53,9 @@ elif echo $args_inst | grep -q -- "--dump-c" ; then fi echo "Running goto-synthesizer: " if echo $args_synthesizer | grep -q -- "--dump-loop-contracts" ; then - $goto_synthesizer ${args_synthesizer} --no-malloc-fail "${name}-mod.gb" + $goto_synthesizer ${args_synthesizer} --no-malloc-may-fail "${name}-mod.gb" else - $goto_synthesizer ${args_synthesizer} --no-malloc-fail "${name}-mod.gb" "${name}-mod-2.gb" + $goto_synthesizer ${args_synthesizer} --no-malloc-may-fail "${name}-mod.gb" "${name}-mod-2.gb" echo "Running CBMC: " $cbmc --no-standard-checks ${args_cbmc} "${name}-mod-2.gb" fi