-
Notifications
You must be signed in to change notification settings - Fork 274
Fix handling of case range statement in special case #3055
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
Fix handling of case range statement in special case #3055
Conversation
Edit: sorry, I should have read the comment on #2905 first. #2905 is merged, this one should now be rebased (and then likely needs more discussion). |
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: a076249).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/86181339
In the case where a gcc case range switch statement has a case that reduces to an empty expression, both gcc and clang reluctantly accept it, producing warnings. CBMC up until now was asserting against that case, and this divergence in behaviour was unwanted.
a076249
to
7685476
Compare
@tautschnig I have rebased it appropriately now. It should be ready for more discussion/review now. |
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.
Could you please add another test case where all/the only case is an empty one? Basically a variant of the existing goto_convert_switch_range_empty test without the default
case.
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: 7685476).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/86275983
@tautschnig Yes, done. |
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: 5da7d4f).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/86295457
In the case where a gcc case range switch statement has a case that reduces to an empty expression, both gcc and clang reluctantly accept it, producing warnings. CBMC up until now was asserting against that case, and this divergence in behaviour was unwanted.