Enable default flags on for checks #8006
Conversation
NlightNFotis
added
the
Version 6
src/cbmc/cbmc_parse_options.cpp
Outdated
| @@ -107,6 +110,20 @@ void cbmc_parse_optionst::set_default_options(optionst &options) | |||
| options.set_option("depth", UINT32_MAX); | |||
| } | |||
|
|
|||
| void cbmc_parse_optionst::set_soundness_on_by_default(optionst &options) | |||
There was a problem hiding this comment.
Please avoid the word "soundness" in this context. It has a specific meaning, and not very much to do with those flags.
There was a problem hiding this comment.
I agree.
I suggest to change it to set_thorough_by_default.
| options.set_option("paths-symex-explore-all", false); | ||
| } else { | ||
| // Not really needed, as it's now on by default, but keeping it here | ||
| // for completeness' sake. |
There was a problem hiding this comment.
Also, please avoid the word "completeness".
There was a problem hiding this comment.
Apologies, I was using the word "completeness" here not in a verification context, but more to indicate symmetry between the two branches (consequent and alternative), despite options setting in one of them being redundant (because the options have been set before we reach the if), so that reading the code is easier compared to leaving the option setting in the context be implicit.
I will update the wording to make this clearer.
|
It's worth remembering that this used to be the default behaviour of CBMC (who's up for some history digging?) What then happened is that all other C analysers did not perform these checks by default, and CBMC looked bad in comparisons. They are expensive (some of the overflow ones even yield nonlinear constraints), and we will need to manage expectations. |
NlightNFotis
force-pushed
the
flags_on_default
branch
4 times, most recently
from
86e159a to
182e44b
Compare
NlightNFotis
requested review from
tautschnig,
peterschrammel,
martin-cs,
thomasspriggs,
TGWDB and
remi-delmas-3000
as code owners
NlightNFotis
changed the title
NlightNFotis
force-pushed
the
flags_on_default
branch
from
182e44b to
f7a9d37
Compare
|
Hello, I'll be closing this one (at least temporarily) in favour of #8093 which is a cleaner version of the change presented here. There are still some changes in this PR that I'd like to see in, but I will see if I can rebase this PR as soon as the other one is in to get a cleaner PR here as well. If that's not possible, then I will incorporate some of these changes into future PRs. |
Enable default analysis flags for CBMC for version 6+.
WIP PR to solicit feedback.
Expect tests broken, most of them are going to require readjusting (regex fixing, and what not).