2121 args_cbmc=" ${args#* " _ " } "
2222fi
2323
24+ dfcc_suffix=" "
2425if [[ " ${use_dfcc} " == " false" ]]; then
2526 set -- $args_inst
2627 args_inst=" "
@@ -32,28 +33,30 @@ if [[ "${use_dfcc}" == "false" ]]; then
3233 shift
3334 fi
3435 done
36+ else
37+ dfcc_suffix=" dfcc"
3538fi
3639
3740if [[ " ${is_windows} " == " true" ]]; then
38- $goto_cc " ${name} .c" " /Fe${name} .gb"
41+ $goto_cc " ${name} .c" " /Fe${name}${dfcc_suffix} .gb"
3942else
40- $goto_cc -o " ${name} .gb" " ${name} .c"
43+ $goto_cc -o " ${name}${dfcc_suffix} .gb" " ${name} .c"
4144fi
4245
43- rm -f " ${name} -mod.gb"
44- $goto_instrument ${args_inst} " ${name} .gb" " ${name} -mod.gb"
45- if [ ! -e " ${name} -mod.gb" ] ; then
46- cp " $name .gb" " ${name} -mod.gb"
46+ rm -f " ${name}${dfcc_suffix} -mod.gb"
47+ $goto_instrument ${args_inst} " ${name}${dfcc_suffix} .gb" " ${name}${dfcc_suffix } -mod.gb"
48+ if [ ! -e " ${name}${dfcc_suffix} -mod.gb" ] ; then
49+ cp " ${ name}${dfcc_suffix} .gb" " ${name}${dfcc_suffix } -mod.gb"
4750elif echo $args_inst | grep -q -- " --dump-c" ; then
48- mv " ${name} -mod.gb" " ${name} -mod.c"
51+ mv " ${name}${dfcc_suffix} -mod.gb" " ${name}${dfcc_suffix } -mod.c"
4952
5053 if [[ " ${is_windows} " == " true" ]]; then
51- $goto_cc " ${name} -mod.c" " /Fe${name} -mod.gb"
54+ $goto_cc " ${name}${dfcc_suffix} -mod.c" " /Fe${name}${dfcc_suffix } -mod.gb"
5255 else
53- $goto_cc -o " ${name} -mod.gb" " ${name} -mod.c"
56+ $goto_cc -o " ${name}${dfcc_suffix} -mod.gb" " ${name}${dfcc_suffix } -mod.c"
5457 fi
5558
56- rm " ${name} -mod.c"
59+ rm " ${name}${dfcc_suffix} -mod.c"
5760fi
58- $goto_instrument --show-goto-functions " ${name} -mod.gb"
59- $cbmc " ${name} -mod.gb" ${args_cbmc}
61+ $goto_instrument --show-goto-functions " ${name}${dfcc_suffix} -mod.gb"
62+ $cbmc " ${name}${dfcc_suffix} -mod.gb" ${args_cbmc}
0 commit comments