Skip to content

Commit 6c26e5a

Browse files
author
Enrico Steffinlongo
committed
Fixed missing typecast in duplicate_per_byte
Function `duplicate_per_byte` checks that the `init_expr` is at max 8-bit wide. However `shadow_memoryt::initialize_shadow_memory` was removing the outer typecast to an 8-bit value, resulting in a call to `duplicate_per_byte` with an `init_expr` larger than 8-bit. This commit removes the typecast removal and fixes the issue.
1 parent 78be04f commit 6c26e5a

File tree

1 file changed

+0
-2
lines changed

1 file changed

+0
-2
lines changed

src/goto-symex/shadow_memory.cpp

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -50,8 +50,6 @@ void shadow_memoryt::initialize_shadow_memory(
5050
else
5151
{
5252
exprt init_expr = field_pair.second;
53-
if(init_expr.id() == ID_typecast)
54-
init_expr = to_typecast_expr(field_pair.second).op();
5553
const auto init_value =
5654
expr_initializer(type, expr.source_location(), ns, init_expr);
5755
CHECK_RETURN(init_value.has_value());

0 commit comments

Comments
 (0)