Open
Description
This issue is to coordinate a major version bump in CBMC. This can include discussion of things to add/change that may be breaking to backwards compatibility, and other related details.
Note that this RFC will be updated routinely ton reflect the discussion, details listed below are not finalised yet!
Major Changes
- Make CBMC's default behaviour "sound". This includes turning on/off appropriate checks and other details so that an out of the box run of CBMC should be as close to correct as possible. Related issues include: RFC: How to handle unsound flags #6480 Unsound command line options should be documented and warnings given when used. #6397
reachability-slice
changes verification from FAILED to SUCCESSFUL #6394 Soundness bug with unconstrained pointers #2617 Goto programs with missing function bodies should not be considered well-formed #1949 - Fix inconsistencies between binaries, e.g.
cbmc
andgoto-instrument
. Related issues: Behavior of infinite loops withgoto-instrument --unwind N --unwinding-assertions
differs fromcbmc --unwind N --unwinding-assertions
#6433 Difference in behavior ofcbmc --unwind N
andgoto-instrument --unwind N
#6432 - Update to C++17 and replace backported STL functions with standard library versions.
- Report more fine grained verification results. Related issues: RFC: How to handle unsound flags #6480
Minor Changes
- Remove deprecated functions
- Array types to contain an index type: introduce index_type and element_type for arrays and vectors #6552