Skip to content

Commit 6e1aa80

Browse files
committed
correctly convert object_address
object_address expressions have pointer type, and hence, the conversion must happen in bv_pointerst::convert_pointer_type.
1 parent 5a16b91 commit 6e1aa80

File tree

1 file changed

+5
-5
lines changed

1 file changed

+5
-5
lines changed

src/solvers/flattening/bv_pointers.cpp

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -410,6 +410,11 @@ bvt bv_pointerst::convert_pointer_type(const exprt &expr)
410410
CHECK_RETURN(bv_opt->size() == bits);
411411
return *bv_opt;
412412
}
413+
else if(expr.id() == ID_object_address)
414+
{
415+
const auto &object_address_expr = to_object_address_expr(expr);
416+
return add_addr(object_address_expr.object_expr());
417+
}
413418
else if(expr.id()==ID_constant)
414419
{
415420
const constant_exprt &c = to_constant_expr(expr);
@@ -734,11 +739,6 @@ bvt bv_pointerst::convert_bitvector(const exprt &expr)
734739

735740
return bv_utils.zero_extension(op0, width);
736741
}
737-
else if(expr.id() == ID_object_address)
738-
{
739-
const auto &object_address_expr = to_object_address_expr(expr);
740-
return add_addr(object_address_expr.object_expr());
741-
}
742742

743743
return SUB::convert_bitvector(expr);
744744
}

0 commit comments

Comments
 (0)