-
Notifications
You must be signed in to change notification settings - Fork 274
Remove ID_C_bounds_check special-case in goto_check_ct #6684
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
Remove ID_C_bounds_check special-case in goto_check_ct #6684
Conversation
Codecov Report
@@ Coverage Diff @@
## develop #6684 +/- ##
===========================================
- Coverage 76.92% 76.82% -0.11%
===========================================
Files 1583 1582 -1
Lines 183314 182760 -554
===========================================
- Hits 141018 140407 -611
- Misses 42296 42353 +57
Continue to review full report at Codecov.
|
e730633
to
a49b771
Compare
The C front-end can safely use the pragma-based approach that is more general.
a49b771
to
4d4f9e7
Compare
The cleanup of 4d4f9e7 (PR diffblue#6684) made bounds checking of these bit count expressions unconditional. This did not affect any input coming from the C front-end, but became apparent with the Rust front-end as documented in model-checking/kani#886. This commit restores conditional bounds checking, but now actually uses the proper expression API rather than the low-level hack.
The cleanup of 4d4f9e7 (PR diffblue#6684) made bounds checking of these bit count expressions unconditional. This did not affect any input coming from the C front-end, but became apparent with the Rust front-end as documented in model-checking/kani#886. This commit restores conditional bounds checking, but now actually uses the proper expression API rather than the low-level hack.
This is never used in the Java front-end, and the C front-end can safely
use the pragma-based approach that is more general.