From bbdfdb1461e0d24b2bbbb795211ddc335a357c54 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Sun, 22 Aug 2021 23:37:00 +0100 Subject: [PATCH] Fix applicability condition of simplify_byte_update The condition is supposed to guard against a crash in basic_string::replace, which it fails to do if the offsets in the condition and the argument to replace don't match. --- src/util/simplify_expr.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp index 9a1f8e8bbf0..e4fc2508780 100644 --- 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);