Commit 9ec216c
committed
Restore conditional bounds-checking of count_{leading,trailing}_zeros
The cleanup of 4d4f9e7 (PR #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.1 parent 3a31976 commit 9ec216c
1 file changed
+4
-1
lines changed| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
1508 | 1508 | | |
1509 | 1509 | | |
1510 | 1510 | | |
1511 | | - | |
| 1511 | + | |
| 1512 | + | |
| 1513 | + | |
| 1514 | + | |
1512 | 1515 | | |
1513 | 1516 | | |
1514 | 1517 | | |
| |||
0 commit comments