search

marek-trtik / cbmc

C Bounded Model Checker
http://www.cprover.org/cbmc
Other
0 stars 0 forks source link

CBMC shell script has different behaviour in different machines/OSs #13

Open lucasccordeiro opened 7 years ago

lucasccordeiro commented 7 years ago

For some unknown reason, the CBMC shell script produces different behaviour in different machines/OS. For instance, for this benchmark cdaudio_simpl1_false-unreach-call_true-valid-memsafety_true-termination.cil.c, our shell script produced ERROR and false(unreach-call) running the Ubuntu OS, but on different machines. On MacOS, the shell script produces true as result.

tautschnig commented 6 years ago

Does CBMC even provide a counterexample on MacOS for this benchmark? I wouldn't be surprised if --32 doesn't actually work on MacOS.

lucasccordeiro commented 6 years ago

I get no counterexample for this benchmark. I think the problem is this warning message:

./cbmc-wrapper: line 50: declare: -A: invalid option
declare: usage: declare [-afFirtx] [-p] [name[=value] ...]

I didn't have a chance to look further at this problem. I think my MacOS does not understand this:

declare -A OPTIONS
OPTIONS["label"]="--error-label"
OPTIONS["unreach_call"]=""
OPTIONS["termination"]=""
OPTIONS["overflow"]="--signed-overflow-check --no-assertions"
OPTIONS["memsafety"]="--pointer-check --memory-leak-check --bounds-check --no-assertions"
tautschnig commented 6 years ago

declare -A requires bash version 4. It would be possible to work around this by instead using multiple variables OPTIONS_label, OPTIONS_unreach_call, etc. and then construct the variable name at the point of use: var=OPTIONS_$PROP ; val=${!var}