-
Notifications
You must be signed in to change notification settings - Fork 274
Add support for gccs __builtin_sub_overflow primitives #5235
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
Add support for gccs __builtin_sub_overflow primitives #5235
Conversation
Codecov Report
@@ Coverage Diff @@
## develop #5235 +/- ##
===========================================
+ Coverage 67.42% 67.42% +<.01%
===========================================
Files 1162 1162
Lines 95606 95606
===========================================
+ Hits 64459 64460 +1
+ Misses 31147 31146 -1
Continue to review full report at Codecov.
|
88d98ef
to
1249404
Compare
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.
Looks good.
1249404
to
0d3f4c9
Compare
Note: Not the generic version
0d3f4c9
to
d33d348
Compare
|
||
\[check_int.assertion.1\] line \d+ assertion !__builtin_ssub_overflow\(1, 1, &result\): SUCCESS | ||
\[check_int.assertion.2\] line \d+ assertion result == 0: SUCCESS | ||
\[check_int.assertion.3\] line \d+ assertion __builtin_ssub_overflow\(.*, 1, &result\): SUCCESS |
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.
In case you’re wondering, the regexes here are due cbmc on travis (and apparently only on travis) “helpfully” expanding macros in assertion messages...
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.
Looks good, thanks!
Note: Not the generic version
More or less the same as #5233, but with
sub
instead ofadd
.