CProver manual
|
In #6480, there has been some extensive conversation about what it means for certain options to produce unsound behavior.
We concluded that unsound in this context is a proxy for the following two behaviors that we want to avoid:
We expect that, by default, CBMC and JBMC display none of the behavior we described above (and if they do, it’s an extremely serious bug that we aim to fix on an ASAP basis), but be aware that certain tools, like goto-instrument
, may contain components that are experimental in nature and thus do transformations that eventually lead to behavior such as the ones described above. Furthermore, some options lead to unsound analysis results by design, and some transformations performed by goto-instrument
will yield verification results that are (by design) unsound when taking verification of the non-transformed program as reference.
The following options will produce a warning when used with CBMC or JBMC:
--unwind
or --unwindset
without --unwinding-assertions
, or the use of --partial-loops
.--depth
, --symex-complexity-limit
).See Understanding Loop Unwinding for an elaboration of these options.
For arrays with unknown length (e.g. input arrays), JBMC has a default limit that can be changed with the option --max-nondet-array-length
.
Be advised that the following command line options to cbmc
and goto-instrument
have been reported to be unsound:
--full-slice
has been reported to be unsound in issue cbmc#260 In particular, --full-slice
appears to lead to spurious counter examples, because values that get assigned by a function whose body gets sliced out are no longer present in the trace, but still result in flipped verification results.cbmc
and goto-instrument
have also been modified to warn that options used are unsound as part of their output. An example of how that output looks is shown below:
Last modified: 2024-11-20 06:00:32 -0800