Update to CBMC 5.11 #151
Merged
Update to CBMC 5.11 #151
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
viktormalik
reviewed
Apr 29, 2021
FrNecas
force-pushed
the
frnecas-cbmc-5.11
branch
from
b4fe4e8 to
fc33f52
Compare
viktormalik
approved these changes
Apr 30, 2021
peterschrammel
approved these changes
Apr 30, 2021
Update expected assertion descriptions (5.10 change) - During analyses of code such as `p->n`, CBMC now creates an assertion that takes the offset of `n` into consideration leading to a different assertion description. Moreover, a new type of check has been added leading to a shift in numbering Adjust domains transform() arguments Adjust to operator() changes in domains Fix function_application_exprt construction Consider optional return value of pointer_offset_size Fix constant_propagator_ait construction Remove setting of lhs_object in goto_trace_stept - The API of the class has changed, the whole lhs_object is no longer stored there, however it can be obtained using get_lhs_object method which uses full_lhs to parse it. Fix goto program loading Fix show_symbol_table call Fix GOTO program output Fix show_goto_trace call Signed-off-by: František Nečas <[email protected]>
Signed-off-by: František Nečas <[email protected]>
|
Should be ready for merge once the tests pass |
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.
2 releases at once this time, since 5.10 required only a small test change (see the commit). The next release is probably going to be tough...
CBMC 5.11 most important changes:
transformnow takes function name,operator()as well. This required changing the passed arguments to various objects/methods in a lot of placesoutputmethod removed from various objects, e.g. fromgoto_modelt, replaced withshow_goto_functionsfunctionlhs_objecthas been removed fromgoto_step_tracet, I am not very confident about my fix in b35aedb ...pointer_offset_sizenow returnsstd::optionalRelated: peterschrammel/cbmc#24