Skip to content

Commit 279c72b

Browse files
smowtonthk123
authored and
thk123
committed
Allocate objects: cast when pointer types differ
It already tried to do this, but doesn't take account for pointers that encode generic information: in such cases the underlying object type can be equal but the pointers differ, and a cast is necessary.
1 parent 3fd321c commit 279c72b

File tree

1 file changed

+2
-6
lines changed

1 file changed

+2
-6
lines changed

src/util/allocate_objects.cpp

Lines changed: 2 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -212,12 +212,8 @@ exprt allocate_objectst::allocate_non_dynamic_object(
212212
aux_symbol.is_static_lifetime = static_lifetime;
213213
symbols_created.push_back(&aux_symbol);
214214

215-
exprt aoe =
216-
ns.follow(aux_symbol.symbol_expr().type()) !=
217-
ns.follow(target_expr.type().subtype())
218-
? (exprt)typecast_exprt(
219-
address_of_exprt(aux_symbol.symbol_expr()), target_expr.type())
220-
: address_of_exprt(aux_symbol.symbol_expr());
215+
exprt aoe = typecast_exprt::conditional_cast(
216+
address_of_exprt(aux_symbol.symbol_expr()), target_expr.type());
221217

222218
code_assignt code(target_expr, aoe);
223219
code.add_source_location() = source_location;

0 commit comments

Comments
 (0)