Introduce symex value set as interface to value set#4778
Closed
romainbrenguier wants to merge 11 commits intodiffblue:developfrom
Closed
Introduce symex value set as interface to value set#4778romainbrenguier wants to merge 11 commits intodiffblue:developfrom
romainbrenguier wants to merge 11 commits intodiffblue:developfrom
Conversation
romainbrenguier
requested review from
chrisr-diffblue,
kroening,
martin-cs,
owen-mc-diffblue,
peterschrammel,
smowton and
tautschnig
as code owners
4 tasks
get_l1_object suggests we are comparing the address of the object, but the actually should interpret the symbol itself as a pointer. A unit test for the case of the issue that is fixed will be added in a following commit.
This can be useful when the type doesn't tell us directly that an exprt has been renamed, but we would expect it to be.
There is no reason for an expression renamed to level 1 to have type renamed to level 2.
This avoids having to import std_expr in the header file
This avoids having to provide a namespace argument and having a default language defined.
This argument is unused.
This is meant to be used in symex as an interface to value_sett instead of accessing value_sett directly. This is to ensure it will be used in a consistent way, in particular regarding the renaming level.
This is required to replace the use of value_sett by symex_value_sett so that we can provide the right type of arguments.
This ensures that in symex the value set are always indexed using l1 renamed symbols.
romainbrenguier
force-pushed
the
clean-up/symex-value-set
branch
from
ded9716 to
711abcc
Compare
Contributor
|
Still wanted? |
Contributor
Author
|
outdated |
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
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 participants
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.
This includes a fix from #4774
This add some checks for an implicit invariant that I noticed while unit testing, makes value_sett::output more usable in particular for debugging unit tests, and define symex_value_sett to act has an interface to value_sett and ensure symex only uses L1 symbols.