Skip to content

Commit 8300147

Browse files
committed
Abort on byte_update(pointer)
Just ignoring them would yield unsound results.
1 parent a695814 commit 8300147

File tree

1 file changed

+6
-0
lines changed

1 file changed

+6
-0
lines changed

src/solvers/flattening/bv_pointers.cpp

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -441,6 +441,12 @@ bvt bv_pointerst::convert_pointer_type(const exprt &expr)
441441
{
442442
return SUB::convert_byte_extract(to_byte_extract_expr(expr));
443443
}
444+
else if(
445+
expr.id() == ID_byte_update_little_endian ||
446+
expr.id() == ID_byte_update_big_endian)
447+
{
448+
throw "byte-wise updates of pointers are unsupported";
449+
}
444450

445451
return conversion_failed(expr);
446452
}

0 commit comments

Comments
 (0)