Update to CBMC 5.8 #149
Merged
Update to CBMC 5.8 #149
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
FrNecas
force-pushed
the
frnecas-cbmc-5.8
branch
from
786bb10 to
8db2947
Compare
viktormalik
requested changes
Mar 18, 2021
FrNecas
force-pushed
the
frnecas-cbmc-5.8
branch
from
8db2947 to
0e31302
Compare
peterschrammel
approved these changes
Mar 25, 2021
src/2ls/2ls_parse_options.h
Outdated
| "(no-spurious-check)(stop-on-fail)" \ | ||
| "(competition-mode)(slice)(no-propagation)(independent-properties)" \ | ||
| "(no-unwinding-assertions)" | ||
| "(constant-propagation)(no-unwinding-assertions)" |
There was a problem hiding this comment.
⛏️ put each declaration on a separate line to reduce merge conflicts in future.
Workaround final keyword in dstringt. Update c_types.h header path. Avoid use of goto_functiont copy constructor. Fix moved attributes from goto_trace_stept to goto_trace_stept::typet. Replace deprecated integer_constant. Fix checking decision_proceduret result. Fix missing ID__start. Fix checking against ui_message_handlert attributes. Fix checking property_checkert result. Fix deprecated status() call. Add message_handler to remove_function_pointers. Fix smt2_convt::Z3 attribute location. Fix unwinding strategy specification. Do not propagate message_handler when it is NULL. Fix SSA assert construction. - CBMC 5.8 added FALSE || to the beginning of instrumented assertions which revealed a flaw in how the assertions were constructed in 2LS. Make the approach more general, recursively going through the whole assertion. Fix CPROVER entrypoint. Remove typedef from test to make it consistent. - Messages from CBMC now contain the typedef instead of the typedef-ed structure, remove typedefs in tests to avoid inconsistencies. Signed-off-by: František Nečas <[email protected]>
This is a temporary commit, constant propagation is broken in CBMC 5.8 (constants are propagated when they should not) which results in incorrect 2LS behaviour. Signed-off-by: František Nečas <[email protected]>
Signed-off-by: František Nečas <[email protected]>
FrNecas
force-pushed
the
frnecas-cbmc-5.8
branch
from
0e31302 to
2411949
Compare
|
Fixed, rebased and squashed, should be ready for merging. |
viktormalik
approved these changes
Mar 26, 2021
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
I will merge this PR similarly to the last one, this time in 3 commits - all the necessary fixes, commit 770d349 (so that we can easily revert it once propagation is fixed) and commit updating version.
Related: peterschrammel/cbmc#22
Changes
FALSE || <assertion>, this required fixes in a0f6f5f to make memsafety work.