-
Notifications
You must be signed in to change notification settings - Fork 30
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
Convert crash on binop to controlled error #461
Conversation
@cp526 I guessed at an error message, but perhaps you can propose something better? |
| _ -> | ||
fail (fun _ -> | ||
{ loc; | ||
msg = Generic !^"M_PEbounded_binop: unsupported on non-integer types" |
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 should probably mention that this is unsupported on anything other than unsigned integers.
... Although I think these might really be proper assertion failures. |
What does it mean for this to be a proper assertion failure? I would assume these should only occur in anomalous states, ie states that should be prevented by some other CN code |
I suspect we're in that kind of situation here: something in CN+Cerberus's earlier logic should prevent an application of Similarly, the M_PEbounded_binop below should only happen on integer types. |
Yes, I think so; I see no reason why CN shouldn't handle the example from #233 . |
Okay, I'm closing this PR - looks like someone should look at the root cause of #233 (I'll take a look but I suspect it's too deep in the stack for my level of understanding) |
Partially addresses #233