Skip to content

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

Merged
merged 1 commit into from
Jan 24, 2019

Conversation

tautschnig
Copy link
Collaborator

Move the implementation from the unit test to object_descriptor_exprt to have
all users of object_descriptor_exprt benefit from it.

  • Each commit message has a non-empty body, explaining why the change was made.
  • n/a Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
  • n/a The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
  • Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
  • n/a My commit message includes data points confirming performance improvements (if claimed).
  • My PR is restricted to a single feature or bugfix.
  • n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

Copy link
Contributor

@allredj allredj left a 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

Copy link
Contributor

@thk123 thk123 left a 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?

@thk123
Copy link
Contributor

thk123 commented Jan 23, 2019

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.

@smowton
Copy link
Contributor

smowton commented Jan 23, 2019

The first case doesn't make sense (the address of something's address isn't a sensible concept), but &*foo is sane

@@ -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))
Copy link
Contributor

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?

Copy link
Collaborator Author

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.

@tautschnig tautschnig force-pushed the use-object_descriptor branch from bb511db to 4b205c8 Compare January 23, 2019 18:08
@tautschnig
Copy link
Collaborator Author

Test and handling of the &*foo case added.

Move the implementation from the unit test to object_descriptor_exprt to have
all users of object_descriptor_exprt benefit from it.
@tautschnig tautschnig force-pushed the use-object_descriptor branch from 4b205c8 to 83af955 Compare January 24, 2019 13:16
Copy link
Contributor

@allredj allredj left a 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.

@tautschnig tautschnig merged commit dc4ffae into diffblue:develop Jan 24, 2019
@tautschnig tautschnig deleted the use-object_descriptor branch January 24, 2019 21:18
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Projects
None yet
Development

Successfully merging this pull request may close these issues.

4 participants