@@ -516,8 +516,6 @@ void value_sett::get_value_set_rec(
516516 std::cout << " GET_VALUE_SET_REC SUFFIX: " << suffix << ' \n ' ;
517517#endif
518518
519- const typet &expr_type=ns.follow (expr.type ());
520-
521519 if (expr.id ()==ID_unknown || expr.id ()==ID_invalid)
522520 {
523521 insert (dest, exprt (ID_unknown, original_type));
@@ -539,17 +537,20 @@ void value_sett::get_value_set_rec(
539537 }
540538 else if (expr.id ()==ID_member)
541539 {
542- const typet &type = ns. follow ( to_member_expr (expr).compound (). type () );
540+ const exprt &compound = to_member_expr (expr).compound ();
543541
544542 DATA_INVARIANT (
545- type.id () == ID_struct || type.id () == ID_union,
543+ compound.type ().id () == ID_struct ||
544+ compound.type ().id () == ID_struct_tag ||
545+ compound.type ().id () == ID_union ||
546+ compound.type ().id () == ID_union_tag,
546547 " compound of member expression must be struct or union" );
547548
548549 const std::string &component_name=
549550 expr.get_string (ID_component_name);
550551
551552 get_value_set_rec (
552- to_member_expr (expr). compound () ,
553+ compound,
553554 dest,
554555 includes_nondet_pointer,
555556 " ." + component_name + suffix,
@@ -559,7 +560,7 @@ void value_sett::get_value_set_rec(
559560 else if (expr.id ()==ID_symbol)
560561 {
561562 auto entry_index = get_index_of_symbol (
562- to_symbol_expr (expr).get_identifier (), expr_type , suffix, ns);
563+ to_symbol_expr (expr).get_identifier (), expr. type () , suffix, ns);
563564
564565 if (entry_index.has_value ())
565566 make_union (dest, find_entry (*entry_index)->object_map );
@@ -624,11 +625,11 @@ void value_sett::get_value_set_rec(
624625 {
625626 insert (
626627 dest,
627- exprt (ID_null_object, to_pointer_type (expr_type ).base_type ()),
628+ exprt (ID_null_object, to_pointer_type (expr. type () ).base_type ()),
628629 mp_integer{0 });
629630 }
630- else if (expr_type. id ()==ID_unsignedbv ||
631- expr_type. id ()== ID_signedbv)
631+ else if (
632+ expr. type (). id () == ID_unsignedbv || expr. type (). id () == ID_signedbv)
632633 {
633634 // an integer constant got turned into a pointer
634635 insert (dest, exprt (ID_integer_address, unsigned_char_type ()));
@@ -703,7 +704,7 @@ void value_sett::get_value_set_rec(
703704 // special case for plus/minus and exactly one pointer
704705 std::optional<exprt> ptr_operand;
705706 if (
706- expr_type .id () == ID_pointer &&
707+ expr. type () .id () == ID_pointer &&
707708 (expr.id () == ID_plus || expr.id () == ID_minus))
708709 {
709710 bool non_const_offset = false ;
@@ -879,10 +880,10 @@ void value_sett::get_value_set_rec(
879880 statement==ID_cpp_new_array)
880881 {
881882 PRECONDITION (suffix.empty ());
882- PRECONDITION (expr_type .id () == ID_pointer);
883+ PRECONDITION (expr. type () .id () == ID_pointer);
883884
884885 dynamic_object_exprt dynamic_object (
885- to_pointer_type (expr_type ).base_type ());
886+ to_pointer_type (expr. type () ).base_type ());
886887 dynamic_object.set_instance (location_number);
887888 dynamic_object.valid ()=true_exprt ();
888889
@@ -893,7 +894,10 @@ void value_sett::get_value_set_rec(
893894 }
894895 else if (expr.id ()==ID_struct)
895896 {
896- const auto &struct_components = to_struct_type (expr_type).components ();
897+ const auto &struct_components =
898+ expr.type ().id () == ID_struct_tag
899+ ? ns.follow_tag (to_struct_tag_type (expr.type ())).components ()
900+ : to_struct_type (expr.type ()).components ();
897901 INVARIANT (
898902 struct_components.size () == expr.operands ().size (),
899903 " struct expression should have an operand per component" );
@@ -950,7 +954,7 @@ void value_sett::get_value_set_rec(
950954
951955 // If the suffix is empty we're looking for the whole struct:
952956 // default to combining both options as below.
953- if (expr_type. id () == ID_struct && !suffix.empty ())
957+ if (expr. type (). id () == ID_struct_tag && !suffix.empty ())
954958 {
955959 irep_idt component_name = with_expr.where ().get (ID_component_name);
956960 if (suffix_starts_with_field (suffix, id2string (component_name)))
@@ -966,7 +970,8 @@ void value_sett::get_value_set_rec(
966970 original_type,
967971 ns);
968972 }
969- else if (to_struct_type (expr_type).has_component (component_name))
973+ else if (ns.follow_tag (to_struct_tag_type (expr.type ()))
974+ .has_component (component_name))
970975 {
971976 // Looking for a non-overwritten member, look through this expression
972977 get_value_set_rec (
@@ -998,7 +1003,7 @@ void value_sett::get_value_set_rec(
9981003 ns);
9991004 }
10001005 }
1001- else if (expr_type .id () == ID_array && !suffix.empty ())
1006+ else if (expr. type () .id () == ID_array && !suffix.empty ())
10021007 {
10031008 std::string new_value_suffix;
10041009 if (has_prefix (suffix, " []" ))
@@ -1105,8 +1110,7 @@ void value_sett::get_value_set_rec(
11051110
11061111 bool found=false ;
11071112
1108- const typet &op_type = ns.follow (byte_extract_expr.op ().type ());
1109- if (op_type.id () == ID_struct)
1113+ if (byte_extract_expr.op ().type ().id () == ID_struct_tag)
11101114 {
11111115 exprt offset = byte_extract_expr.offset ();
11121116 if (eval_pointer_offset (offset, ns))
@@ -1115,7 +1119,8 @@ void value_sett::get_value_set_rec(
11151119 const auto offset_int = numeric_cast<mp_integer>(offset);
11161120 const auto type_size = pointer_offset_size (expr.type (), ns);
11171121
1118- const struct_typet &struct_type = to_struct_type (op_type);
1122+ const struct_typet &struct_type =
1123+ ns.follow_tag (to_struct_tag_type (byte_extract_expr.op ().type ()));
11191124
11201125 for (const auto &c : struct_type.components ())
11211126 {
@@ -1150,10 +1155,13 @@ void value_sett::get_value_set_rec(
11501155 }
11511156 }
11521157
1153- if (op_type. id () == ID_union )
1158+ if (byte_extract_expr. op (). type (). id () == ID_union_tag )
11541159 {
11551160 // just collect them all
1156- for (const auto &c : to_union_type (op_type).components ())
1161+ const auto &components =
1162+ ns.follow_tag (to_union_tag_type (byte_extract_expr.op ().type ()))
1163+ .components ();
1164+ for (const auto &c : components)
11571165 {
11581166 const irep_idt &name = c.get_name ();
11591167 member_exprt member (byte_extract_expr.op (), name, c.type ());
@@ -1429,13 +1437,12 @@ void value_sett::get_reference_set_rec(
14291437 // We cannot introduce a cast from scalar to non-scalar,
14301438 // thus, we can only adjust the types of structs and unions.
14311439
1432- const typet &final_object_type = ns.follow (object.type ());
1433-
1434- if (final_object_type.id ()==ID_struct ||
1435- final_object_type.id ()==ID_union)
1440+ if (
1441+ object.type ().id () == ID_struct_tag ||
1442+ object.type ().id () == ID_union_tag)
14361443 {
14371444 // adjust type?
1438- if (ns. follow ( struct_op.type ())!=final_object_type )
1445+ if (struct_op.type () != object. type () )
14391446 {
14401447 member_expr.compound () =
14411448 typecast_exprt (member_expr.compound (), struct_op.type ());
@@ -1478,11 +1485,10 @@ void value_sett::assign(
14781485 output (std::cout);
14791486#endif
14801487
1481- const typet &type=ns.follow (lhs.type ());
1482-
1483- if (type.id () == ID_struct)
1488+ if (lhs.type ().id () == ID_struct_tag)
14841489 {
1485- for (const auto &c : to_struct_type (type).components ())
1490+ for (const auto &c :
1491+ ns.follow_tag (to_struct_tag_type (lhs.type ())).components ())
14861492 {
14871493 const typet &subtype = c.type ();
14881494 const irep_idt &name = c.get_name ();
@@ -1513,12 +1519,14 @@ void value_sett::assign(
15131519 " rhs.type():\n " +
15141520 rhs.type ().pretty () + " \n " + " lhs.type():\n " + lhs.type ().pretty ());
15151521
1516- const typet &followed = ns.follow (rhs.type ());
1517-
1518- if (followed.id () == ID_struct || followed.id () == ID_union)
1522+ if (rhs.type ().id () == ID_struct_tag || rhs.type ().id () == ID_union_tag)
15191523 {
15201524 const struct_union_typet &rhs_struct_union_type =
1521- to_struct_union_type (followed);
1525+ rhs.type ().id () == ID_struct_tag
1526+ ? static_cast <const struct_union_typet &>(
1527+ ns.follow_tag (to_struct_tag_type (rhs.type ())))
1528+ : static_cast <const struct_union_typet &>(
1529+ ns.follow_tag (to_union_tag_type (rhs.type ())));
15221530
15231531 const typet &rhs_subtype = rhs_struct_union_type.component_type (name);
15241532 rhs_member = simplify_expr (member_exprt{rhs, name, rhs_subtype}, ns);
@@ -1528,30 +1536,30 @@ void value_sett::assign(
15281536 }
15291537 }
15301538 }
1531- else if (type.id ()== ID_array)
1539+ else if (lhs. type () .id () == ID_array)
15321540 {
15331541 const index_exprt lhs_index (
15341542 lhs,
15351543 exprt (ID_unknown, c_index_type ()),
1536- to_array_type (type).element_type ());
1544+ to_array_type (lhs. type () ).element_type ());
15371545
15381546 if (rhs.id ()==ID_unknown ||
15391547 rhs.id ()==ID_invalid)
15401548 {
15411549 assign (
15421550 lhs_index,
1543- exprt (rhs.id (), to_array_type (type).element_type ()),
1551+ exprt (rhs.id (), to_array_type (lhs. type () ).element_type ()),
15441552 ns,
15451553 is_simplified,
15461554 add_to_sets);
15471555 }
15481556 else
15491557 {
15501558 DATA_INVARIANT (
1551- rhs.type () == type,
1559+ rhs.type () == lhs. type () ,
15521560 " value_sett::assign types should match, got: "
15531561 " rhs.type():\n " +
1554- rhs.type ().pretty () + " \n " + " type:\n " + type.pretty ());
1562+ rhs.type ().pretty () + " \n " + " type:\n " + lhs. type () .pretty ());
15551563
15561564 if (rhs.id ()==ID_array_of)
15571565 {
@@ -1575,7 +1583,7 @@ void value_sett::assign(
15751583 const index_exprt op0_index (
15761584 to_with_expr (rhs).old (),
15771585 exprt (ID_unknown, c_index_type ()),
1578- to_array_type (type).element_type ());
1586+ to_array_type (lhs. type () ).element_type ());
15791587
15801588 assign (lhs_index, op0_index, ns, is_simplified, add_to_sets);
15811589 assign (
@@ -1586,7 +1594,7 @@ void value_sett::assign(
15861594 const index_exprt rhs_index (
15871595 rhs,
15881596 exprt (ID_unknown, c_index_type ()),
1589- to_array_type (type).element_type ());
1597+ to_array_type (lhs. type () ).element_type ());
15901598 assign (lhs_index, rhs_index, ns, is_simplified, true );
15911599 }
15921600 }
@@ -1683,15 +1691,15 @@ void value_sett::assign_rec(
16831691 {
16841692 const auto &lhs_member_expr = to_member_expr (lhs);
16851693 const auto &component_name = lhs_member_expr.get_component_name ();
1686-
1687- const typet &type = ns.follow (lhs_member_expr.compound ().type ());
1694+ const exprt &compound = lhs_member_expr.compound ();
16881695
16891696 DATA_INVARIANT (
1690- type.id () == ID_struct || type.id () == ID_union,
1697+ compound.type ().id () == ID_struct_tag ||
1698+ compound.type ().id () == ID_union_tag,
16911699 " operand 0 of member expression must be struct or union" );
16921700
16931701 assign_rec (
1694- lhs_member_expr. compound () ,
1702+ compound,
16951703 values_rhs,
16961704 " ." + id2string (component_name) + suffix,
16971705 ns,
0 commit comments