-
Notifications
You must be signed in to change notification settings - Fork 273
Byte-operator lowering: do not generate type casts to compound types [blocks: #2068] #4227
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
} | ||
else if(target_type.id() == ID_string) | ||
{ | ||
// this works, but is somewhat questionable |
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.
Clarify why?
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.
Why it works or why it is questionable?
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.
Why it's questionable
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.
Because the only ID_string
-typed expression we really deal with is a constant_exprt
. But all tests pass when I do this 👼
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: 175c12c).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/101421426
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.
Please break this big function into parts and document it. It will then be easier to review.
else | ||
{ | ||
PRECONDITION_WITH_DIAGNOSTICS( | ||
false, "bv_to_expr does not yet support ", target_type.id_string()); |
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.
That's not a precondition, use UNEXPECTEDCASE
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.
There is UNHANDLED_CASE
, but the documentation suggests that this should not be used, and it wouldn't provide diagnostics either. So I'm inclined to leave this as is.
These aren't fully supported by the back-ends. Instead, bit-extract the components and construct an expression.
175c12c
to
131fda0
Compare
Refactored and acted upon comments as far as possible. @owen-jones-diffblue @romainbrenguier @smowton could you please take another look? |
These aren't fully supported by the back-ends. Instead, bit-extract the
components and construct an expression.