From 9ec216c4c6653446f1107e2995078f84e2192c19 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 4 Mar 2022 22:20:36 +0000 Subject: [PATCH] Restore conditional bounds-checking of count_{leading,trailing}_zeros The cleanup of 4d4f9e7d182 (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. --- src/ansi-c/goto_check_c.cpp | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/ansi-c/goto_check_c.cpp b/src/ansi-c/goto_check_c.cpp index 3826177edaa..28242fd658d 100644 --- a/src/ansi-c/goto_check_c.cpp +++ b/src/ansi-c/goto_check_c.cpp @@ -1508,7 +1508,10 @@ void goto_check_ct::bounds_check(const exprt &expr, const guardt &guard) if(expr.id() == ID_index) bounds_check_index(to_index_expr(expr), guard); else if( - expr.id() == ID_count_leading_zeros || expr.id() == ID_count_trailing_zeros) + (expr.id() == ID_count_leading_zeros && + !to_count_leading_zeros_expr(expr).zero_permitted()) || + (expr.id() == ID_count_trailing_zeros && + !to_count_trailing_zeros_expr(expr).zero_permitted())) { bounds_check_bit_count(to_unary_expr(expr), guard); }