File tree 3 files changed +9
-5
lines changed
3 files changed +9
-5
lines changed Original file line number Diff line number Diff line change 43
43
$goto_cc -o " ${name}${dfcc_suffix} .gb" " ${name} .c"
44
44
fi
45
45
46
+ if [[ " ${args_inst} " != * " malloc" * ]]; then
47
+ args_inst=" --no-malloc-fail $args_inst "
48
+ fi
49
+
46
50
rm -f " ${name}${dfcc_suffix} -mod.gb"
47
51
$goto_instrument ${args_inst} " ${name}${dfcc_suffix} .gb" " ${name}${dfcc_suffix} -mod.gb"
48
52
if [ ! -e " ${name}${dfcc_suffix} -mod.gb" ] ; then
Original file line number Diff line number Diff line change 21
21
fi
22
22
23
23
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"
25
25
if [ ! -e " ${target} -mod.gb" ] ; then
26
26
cp " ${target} .gb" " ${target} -mod.gb"
27
27
elif echo $args | grep -q -- " --dump-c-type-header" ; then
@@ -39,5 +39,5 @@ elif echo $args | grep -q -- "--dump-c" ; then
39
39
40
40
rm " ${target} -mod.c"
41
41
fi
42
- $goto_instrument --show-goto-functions " ${target} -mod.gb"
42
+ $goto_instrument --no-malloc-fail -- show-goto-functions " ${target} -mod.gb"
43
43
$cbmc --no-standard-checks " ${target} -mod.gb"
Original file line number Diff line number Diff line change 37
37
rm -f " ${name} -mod.gb"
38
38
rm -f " ${name} -mod-2.gb"
39
39
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"
41
41
if [ ! -e " ${name} -mod.gb" ] ; then
42
42
cp " $name .gb" " ${name} -mod.gb"
43
43
elif echo $args_inst | grep -q -- " --dump-c" ; then
@@ -53,9 +53,9 @@ elif echo $args_inst | grep -q -- "--dump-c" ; then
53
53
fi
54
54
echo " Running goto-synthesizer: "
55
55
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"
57
57
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"
59
59
echo " Running CBMC: "
60
60
$cbmc --no-standard-checks ${args_cbmc} " ${name} -mod-2.gb"
61
61
fi
You can’t perform that action at this time.
0 commit comments