@@ -239,18 +239,19 @@ std::optional<bvt> bv_pointers_widet::convert_address_of_rec(const exprt &expr)
239239 {
240240 const member_exprt &member_expr = to_member_expr (expr);
241241 const exprt &struct_op = member_expr.compound ();
242- const typet &struct_op_type = ns.follow (struct_op.type ());
243242
244243 // recursive call
245244 auto bv_opt = convert_address_of_rec (struct_op);
246245 if (!bv_opt.has_value ())
247246 return {};
248247
249248 bvt bv = std::move (*bv_opt);
250- if (struct_op_type. id () == ID_struct )
249+ if (struct_op. type (). id () == ID_struct_tag )
251250 {
252251 auto offset = member_offset (
253- to_struct_type (struct_op_type), member_expr.get_component_name (), ns);
252+ ns.follow_tag (to_struct_tag_type (struct_op.type ())),
253+ member_expr.get_component_name (),
254+ ns);
254255 CHECK_RETURN (offset.has_value ());
255256
256257 // add offset
@@ -260,7 +261,7 @@ std::optional<bvt> bv_pointers_widet::convert_address_of_rec(const exprt &expr)
260261 else
261262 {
262263 INVARIANT (
263- struct_op_type. id () == ID_union ,
264+ struct_op. type (). id () == ID_union_tag ,
264265 " member expression should operate on struct or union" );
265266 // nothing to do, all members have offset 0
266267 }
@@ -499,21 +500,22 @@ bvt bv_pointers_widet::convert_pointer_type(const exprt &expr)
499500 else if (expr.id () == ID_field_address)
500501 {
501502 const auto &field_address_expr = to_field_address_expr (expr);
502- const typet &compound_type = ns.follow (field_address_expr.compound_type ());
503503
504504 // recursive call
505505 auto bv = convert_bitvector (field_address_expr.base ());
506506
507- if (compound_type.id () == ID_struct )
507+ if (field_address_expr. compound_type () .id () == ID_struct_tag )
508508 {
509509 auto offset = member_offset (
510- to_struct_type (compound_type), field_address_expr.component_name (), ns);
510+ ns.follow_tag (to_struct_tag_type (field_address_expr.compound_type ())),
511+ field_address_expr.component_name (),
512+ ns);
511513 CHECK_RETURN (offset.has_value ());
512514
513515 // add offset
514516 bv = offset_arithmetic (field_address_expr.type (), bv, *offset);
515517 }
516- else if (compound_type.id () == ID_union )
518+ else if (field_address_expr. compound_type () .id () == ID_union_tag )
517519 {
518520 // nothing to do, all fields have offset 0
519521 }
0 commit comments