Update to CBMC 5.9 #150
Merged
Update to CBMC 5.9 #150
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
peterschrammel
approved these changes
Apr 16, 2021
| class twols_parse_optionst: | ||
| public parse_options_baset, | ||
| public language_uit | ||
| public messaget |
There was a problem hiding this comment.
💡 Preferably add a messaget log member than deriving from messaget.
There was a problem hiding this comment.
I wanted to follow CBMC's example (cbmc_parse_optionst used to inherit from language_uit and now inherits from messaget). Moving from inheritance to a member would require a lot of changes throughout the whole module, so I'd rather keep it as is for now to keep the changes minimal.
FrNecas
force-pushed
the
frnecas-cbmc-5.9
branch
from
4936f5f to
3599325
Compare
viktormalik
reviewed
Apr 19, 2021
FrNecas
force-pushed
the
frnecas-cbmc-5.9
branch
from
3599325 to
aa7acfc
Compare
viktormalik
approved these changes
Apr 19, 2021
|
Please update the submodule pointer and merge. |
Fix adjust_float_expressions include Fix bv_refinementt creation Add missing is_bottom and is_top methods Replace ID_malloc with ID_allocate Assign symbol_expr to function_application_exprt Replace deprecated forall_symbols FIx pointer_type creation Fix construction of address_of_exprt Convert ns.lookup argument to symbol_exprt Correctly construct pointer types Convert union_find from inheritance to attribute Fix langapi include Get rid of unused and deprecated time measuring Do not mention CBMC_VERSION in help - The header file cbmc/version.h has been removed and the version is now provided in the build process making it not possible to reference it in 2LS. Simplify GOTO program reading - CBMC 5.9 introduced a convenient API to parse the source program into a goto_modelt, make use of the API, simplify 2LS program reading. Also enable --show-symbol-table option Fix JSON trace outputting Remove deprecated java_bytecode include Fix write_goto_binary call Fix make_goto call Update symbol table manipulation Replace deprecated goto_functions_template Link unwindset Make malloc-related modifications more robust Revert "Disable constant propagation by default"
Signed-off-by: František Nečas <[email protected]>
Temporary commit, CBMC 5.9 introduced internal changes to built-in functions (such as malloc and free) breaking one of the assertions. Fixing this will likely be complicated and may be prone to changes in other versions. 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.9
branch
from
aa7acfc to
6941059
Compare
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.
Related: peterschrammel/cbmc#23
Changes:
Also memsafety tests which are correct are broken (one of the assertions failed). We tried to investigate the problem with @viktormalik and it seems to be related to changes in CBMC free implementation. Fixing this may be difficult so we agreed that it may be a good idea to leave it for a stable version (once the rebase is finished).