Skip to content

Commit e334f8b

Browse files
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 dbc5d5d commit e334f8b

File tree

1 file changed

+4
-1
lines changed

1 file changed

+4
-1
lines changed

src/analyses/goto_check_c.cpp

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1508,7 +1508,10 @@ void goto_check_ct::bounds_check(const exprt &expr, const guardt &guard)
15081508
if(expr.id() == ID_index)
15091509
bounds_check_index(to_index_expr(expr), guard);
15101510
else if(
1511-
expr.id() == ID_count_leading_zeros || expr.id() == ID_count_trailing_zeros)
1511+
(expr.id() == ID_count_leading_zeros &&
1512+
!to_count_leading_zeros_expr(expr).zero_permitted()) ||
1513+
(expr.id() == ID_count_trailing_zeros &&
1514+
!to_count_trailing_zeros_expr(expr).zero_permitted()))
15121515
{
15131516
bounds_check_bit_count(to_unary_expr(expr), guard);
15141517
}

0 commit comments

Comments
 (0)