-
Notifications
You must be signed in to change notification settings - Fork 273
Extend object_descriptor_exprt::build and use it #3898
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Conversation
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
✔️
Passed Diffblue compatibility checks (cbmc commit: bb511db).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/98325399
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This doesn't handle the case of
**&&foo
or
&*foo // foo is a pointer
but I suppose these cases don't happen in reality?
Not blocking - but now would be a great time to add some unit tests for this utility which would serve both as testing but also documentation for how it can be used. |
The first case doesn't make sense (the address of something's address isn't a sensible concept), but |
@@ -114,6 +113,15 @@ static void build_object_descriptor_rec( | |||
|
|||
build_object_descriptor_rec(ns, tc.op(), dest); | |||
} | |||
else if(const auto deref = expr_try_dynamic_cast<dereference_exprt>(expr)) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Maybe briefly comment why this isn't a task for the simplifier?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This is something the simplifier should cover, but this piece of code should be usable irrespective of whether an expression has been simplified or not.
bb511db
to
4b205c8
Compare
Test and handling of the |
Move the implementation from the unit test to object_descriptor_exprt to have all users of object_descriptor_exprt benefit from it.
4b205c8
to
83af955
Compare
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
🚫
This PR failed Diffblue compatibility checks (cbmc commit: 83af955).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/98479178
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.
Common spurious failures:
- the cbmc commit has disappeared in the mean time (e.g. in a force-push)
- the author is not in the list of contributors (e.g. first-time contributors).
The incompatibility may have been introduced by an earlier PR. In that case merging this
PR should be avoided unless it fixes the current incompatibility.
Move the implementation from the unit test to object_descriptor_exprt to have
all users of object_descriptor_exprt benefit from it.