Skip to content

Commit 20e3767

Browse files
esteffinEnrico Steffinlongo
authored and
Enrico Steffinlongo
committed
Removed extra arguments from goto-instrument regression and added mechanism to pass arguments to cbmc
1 parent c6a65a8 commit 20e3767

File tree

1 file changed

+12
-3
lines changed

1 file changed

+12
-3
lines changed

regression/goto-instrument/chain.sh

Lines changed: 12 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -10,6 +10,15 @@ is_windows=$4
1010
sources=${*:$#}
1111
args=${*:5:$#-5}
1212

13+
if [[ "$args" != *" _ "* ]]
14+
then
15+
args_inst=$args
16+
args_cbmc=""
17+
else
18+
args_inst="${args%%" _ "*}"
19+
args_cbmc="${args#*" _ "}"
20+
fi
21+
1322
set -- $sources
1423
target=${*:$#}
1524
target=${target%.c}
@@ -21,7 +30,7 @@ else
2130
fi
2231

2332
rm -f "${target}-mod.gb"
24-
$goto_instrument --no-malloc-may-fail ${args} "${target}.gb" "${target}-mod.gb"
33+
$goto_instrument ${args_inst} "${target}.gb" "${target}-mod.gb"
2534
if [ ! -e "${target}-mod.gb" ] ; then
2635
cp "${target}.gb" "${target}-mod.gb"
2736
elif echo $args | grep -q -- "--dump-c-type-header" ; then
@@ -39,5 +48,5 @@ elif echo $args | grep -q -- "--dump-c" ; then
3948

4049
rm "${target}-mod.c"
4150
fi
42-
$goto_instrument --no-malloc-may-fail --show-goto-functions "${target}-mod.gb"
43-
$cbmc --no-standard-checks "${target}-mod.gb"
51+
$goto_instrument --show-goto-functions "${target}-mod.gb"
52+
$cbmc ${args_cbmc} "${target}-mod.gb"

0 commit comments

Comments
 (0)