We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent a695814 commit 8300147Copy full SHA for 8300147
src/solvers/flattening/bv_pointers.cpp
@@ -441,6 +441,12 @@ bvt bv_pointerst::convert_pointer_type(const exprt &expr)
441
{
442
return SUB::convert_byte_extract(to_byte_extract_expr(expr));
443
}
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
+ }
450
451
return conversion_failed(expr);
452
0 commit comments