disambiguate two exprts with same ID #4479
Merged
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
owen-mc-diffblue
requested review from
allredj,
chrisr-diffblue,
danpoe,
kroening,
martin-cs,
peterschrammel,
pkesseli,
romainbrenguier,
smowton,
tautschnig and
thk123
as code owners
smowton
approved these changes
Apr 2, 2019
src/util/irep_ids.def
Outdated
| @@ -217,7 +217,7 @@ IREP_ID_ONE(invalid) | |||
| IREP_ID_TWO(C_invalid_object, #invalid_object) | |||
| IREP_ID_ONE(pointer_offset) | |||
| IREP_ID_ONE(pointer_object) | |||
| IREP_ID_TWO(is_invalid_pointer, is-invalid-pointer) | |||
| IREP_ID_TWO(is_invalid_pointer, is_invalid_pointer) | |||
owen-mc-diffblue
force-pushed
the
fix/disambiguate-two-exprts-with-same-id
branch
from
092802b to
a6b6ddb
Compare
This commit resolves an issue where ID_dynamic_object was used to label two semantically distinct exprts. One, with a single operand, was a boolean expression meaning that the operand is a pointer to a dynamic object. This has been renamed to ID_is_dynamic_object. The second, with two operands, is an exprt representing a dynamic object itself. This has stayed ID_dynamic_object. Disambiguating which meaning was intended in each case was relatively easy, as uses of these exprts frequently come with assertions about the number of operands, and so this was used to inform which instances of ID_dynamic_object should be changed and which should be left the same.
This is a more accurate name
owen-mc-diffblue
force-pushed
the
fix/disambiguate-two-exprts-with-same-id
branch
from
a6b6ddb to
e4d3ac6
Compare
allredj
reviewed
Apr 2, 2019
There was a problem hiding this comment.
✔️
Passed Diffblue compatibility checks (cbmc commit: e4d3ac6).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/106816492
tautschnig
approved these changes
Apr 3, 2019
src/util/pointer_predicates.h
Outdated
| @@ -12,6 +12,7 @@ Author: Daniel Kroening, [email protected] | |||
| #ifndef CPROVER_UTIL_POINTER_PREDICATES_H | |||
| #define CPROVER_UTIL_POINTER_PREDICATES_H | |||
|
|
|||
| #include "std_expr.h" | |||
| #define SYMEX_DYNAMIC_PREFIX "symex_dynamic::" | |||
|
|
|||
| class exprt; | |||
There was a problem hiding this comment.
Some of those forward declarations will now be unnecessary given the added include.
src/util/pointer_predicates.h
Outdated
| @@ -33,7 +33,6 @@ exprt good_pointer_def(const exprt &pointer, const namespacet &); | |||
| exprt null_object(const exprt &pointer); | |||
| exprt null_pointer(const exprt &pointer); | |||
| exprt integer_address(const exprt &pointer); | |||
| exprt is_invalid_pointer(const exprt &pointer); | |||
There was a problem hiding this comment.
I guess that's ok, though generally we should first mark such functions as deprecated.
added 3 commits
April 3, 2019 09:40
This matches the things around it better.
owen-mc-diffblue
force-pushed
the
fix/disambiguate-two-exprts-with-same-id
branch
from
e4d3ac6 to
a9774ca
Compare
allredj
reviewed
Apr 3, 2019
There was a problem hiding this comment.
✔️
Passed Diffblue compatibility checks (cbmc commit: a9774ca).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/106877160
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.
The first commit is cherry-picked from #2646. I thought it deserved to be merged, even if the rest of that PR is not being worked on. I also implemented a suggestion from @smowton on that PR to make a new class
is_invalid_pointer_exprt. The same could be done for many other pointer predicates, but I do not have time right now.