Fix value-set make_member function #3570
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
smowton
requested review from
chrisr-diffblue,
kroening,
martin-cs,
peterschrammel,
pkesseli and
tautschnig
as code owners
smowton
changed the title
smowton
force-pushed
the
smowton/fix/value-set-member-type-safety
branch
from
26626ad to
142cafe
Compare
allredj
reviewed
Dec 17, 2018
There was a problem hiding this comment.
✔️
Passed Diffblue compatibility checks (cbmc commit: 142cafe).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/94978728
smowton
force-pushed
the
smowton/fix/value-set-member-type-safety
branch
from
142cafe to
9d6260f
Compare
tautschnig
approved these changes
Dec 17, 2018
|
|
||
| return std::move(member_expr); | ||
| return member_expr; |
There was a problem hiding this comment.
I believe this should stay as return std::move(member_expr);
There was a problem hiding this comment.
Not so! It's type now matches the return type, so I leave it out and enable RVO. I hope a forthcoming version of C++ renders this distinction unnecessary...
There was a problem hiding this comment.
Oops, sorry, I ignored that you had used exprt member_expr ....
…r casts This signals that the cast is cleaner than a general byte-extract a little more clearly
Previously this would simplify ((struct A)x).y into x.y regardless of whether the two structures both have a member y, or whether it is colocated in the two types. Now that the simplifier can soundly simplify such an expression we should just use that instead.
Now that value-set soundly simplifies member-of-cast-of-struct, this test works as expected. This also improves the specificity of the two tests in this directory. This is disabled under SMT2 for the same reason as the existing test.desc -- it involves a struct-to-struct cast, which SMT2's `convert_typecast` doesn't handle yet.
smowton
force-pushed
the
smowton/fix/value-set-member-type-safety
branch
from
9d6260f to
8d88c97
Compare
allredj
reviewed
Dec 17, 2018
There was a problem hiding this comment.
✔️
Passed Diffblue compatibility checks (cbmc commit: 8d88c97).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/94987938
peterschrammel
approved these changes
Dec 17, 2018
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.
Fixes #3569;
depends on #3562, which is the first commit in this PR.Previously
value_settwould simplify ((struct A)x).y into x.y regardless of whether the two structures both have a member y, or whether it is colocated in the two types. Improve the simplifier slightly to tackle this case, then use it rather than implement custom logic invalue_sett.