Merge pull request #6708 from tautschnig/bugfixes/cltz-bounds-check

tautschnig · web-flow · commit 0054d51c3435 · 2022-03-08T14:29:19.000+01:00
Restore conditional bounds-checking of count_{leading,trailing}_zeros
diff --git 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);
   }

Original file line number	Diff line number	Diff line change
`@@ -1508,7 +1508,10 @@ void goto_check_ct::bounds_check(const exprt &expr, const guardt &guard)`
`1508`	`1508`	`if(expr.id() == ID_index)`
`1509`	`1509`	`bounds_check_index(to_index_expr(expr), guard);`
`1510`	`1510`	`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()))`
`1512`	`1515`	`{`
`1513`	`1516`	`bounds_check_bit_count(to_unary_expr(expr), guard);`
`1514`	`1517`	`}`