Merge pull request #6311 from peterschrammel/fix-simplify-byte-update

peterschrammel · web-flow · commit 14d35cc657dd · 2021-09-13T14:19:40.000+01:00
Fix applicability condition of simplify_byte_update
diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp
@@ -1880,7 +1880,7 @@ simplify_exprt::simplify_byte_update(const byte_update_exprt &expr)
   if(
     root_size.has_value() && *root_size >= 0 && val_size.has_value() &&
     *val_size >= 0 && offset_int.has_value() && *offset_int >= 0 &&
-    *offset_int + *val_size <= *root_size)
+    *offset_int * 8 + *val_size <= *root_size)
   {
     auto root_bits =
       expr2bits(root, expr.id() == ID_byte_update_little_endian, ns);

Original file line number	Diff line number	Diff line change
`@@ -1880,7 +1880,7 @@ simplify_exprt::simplify_byte_update(const byte_update_exprt &expr)`
`1880`	`1880`	`if(`
`1881`	`1881`	`root_size.has_value() && *root_size >= 0 && val_size.has_value() &&`
`1882`	`1882`	`val_size >= 0 && offset_int.has_value() && offset_int >= 0 &&`
`1883`		`- offset_int + val_size <= *root_size)`
	`1883`	`+ offset_int 8 + val_size <= root_size)`
`1884`	`1884`	`{`
`1885`	`1885`	`auto root_bits =`
`1886`	`1886`	`expr2bits(root, expr.id() == ID_byte_update_little_endian, ns);`