@@ -516,8 +516,6 @@ void value_sett::get_value_set_rec(
516
516
std::cout << " GET_VALUE_SET_REC SUFFIX: " << suffix << ' \n ' ;
517
517
#endif
518
518
519
- const typet &expr_type=ns.follow (expr.type ());
520
-
521
519
if (expr.id ()==ID_unknown || expr.id ()==ID_invalid)
522
520
{
523
521
insert (dest, exprt (ID_unknown, original_type));
@@ -539,17 +537,18 @@ void value_sett::get_value_set_rec(
539
537
}
540
538
else if (expr.id ()==ID_member)
541
539
{
542
- const typet &type = ns. follow ( to_member_expr (expr).compound (). type () );
540
+ const exprt & compound = to_member_expr (expr).compound ();
543
541
544
542
DATA_INVARIANT (
545
- type.id () == ID_struct || type.id () == ID_union,
543
+ compound .type ().id () == ID_struct_tag ||
544
+ compound .type ().id () == ID_union_tag,
546
545
" compound of member expression must be struct or union" );
547
546
548
547
const std::string &component_name=
549
548
expr.get_string (ID_component_name);
550
549
551
550
get_value_set_rec (
552
- to_member_expr (expr). compound () ,
551
+ compound ,
553
552
dest,
554
553
includes_nondet_pointer,
555
554
" ." + component_name + suffix,
@@ -559,7 +558,7 @@ void value_sett::get_value_set_rec(
559
558
else if (expr.id ()==ID_symbol)
560
559
{
561
560
auto entry_index = get_index_of_symbol (
562
- to_symbol_expr (expr).get_identifier (), expr_type , suffix, ns);
561
+ to_symbol_expr (expr).get_identifier (), expr. type () , suffix, ns);
563
562
564
563
if (entry_index.has_value ())
565
564
make_union (dest, find_entry (*entry_index)->object_map );
@@ -624,11 +623,11 @@ void value_sett::get_value_set_rec(
624
623
{
625
624
insert (
626
625
dest,
627
- exprt (ID_null_object, to_pointer_type (expr_type ).base_type ()),
626
+ exprt (ID_null_object, to_pointer_type (expr. type () ).base_type ()),
628
627
mp_integer{0 });
629
628
}
630
- else if (expr_type. id ()==ID_unsignedbv ||
631
- expr_type. id ()== ID_signedbv)
629
+ else if (
630
+ expr. type (). id () == ID_unsignedbv || expr. type (). id () == ID_signedbv)
632
631
{
633
632
// an integer constant got turned into a pointer
634
633
insert (dest, exprt (ID_integer_address, unsigned_char_type ()));
@@ -703,7 +702,7 @@ void value_sett::get_value_set_rec(
703
702
// special case for plus/minus and exactly one pointer
704
703
std::optional<exprt> ptr_operand;
705
704
if (
706
- expr_type .id () == ID_pointer &&
705
+ expr. type () .id () == ID_pointer &&
707
706
(expr.id () == ID_plus || expr.id () == ID_minus))
708
707
{
709
708
bool non_const_offset = false ;
@@ -879,10 +878,10 @@ void value_sett::get_value_set_rec(
879
878
statement==ID_cpp_new_array)
880
879
{
881
880
PRECONDITION (suffix.empty ());
882
- PRECONDITION (expr_type .id () == ID_pointer);
881
+ PRECONDITION (expr. type () .id () == ID_pointer);
883
882
884
883
dynamic_object_exprt dynamic_object (
885
- to_pointer_type (expr_type ).base_type ());
884
+ to_pointer_type (expr. type () ).base_type ());
886
885
dynamic_object.set_instance (location_number);
887
886
dynamic_object.valid ()=true_exprt ();
888
887
@@ -893,7 +892,8 @@ void value_sett::get_value_set_rec(
893
892
}
894
893
else if (expr.id ()==ID_struct)
895
894
{
896
- const auto &struct_components = to_struct_type (expr_type).components ();
895
+ const auto &struct_components =
896
+ ns.follow_tag (to_struct_tag_type (expr.type ())).components ();
897
897
INVARIANT (
898
898
struct_components.size () == expr.operands ().size (),
899
899
" struct expression should have an operand per component" );
@@ -950,7 +950,7 @@ void value_sett::get_value_set_rec(
950
950
951
951
// If the suffix is empty we're looking for the whole struct:
952
952
// default to combining both options as below.
953
- if (expr_type. id () == ID_struct && !suffix.empty ())
953
+ if (expr. type (). id () == ID_struct_tag && !suffix.empty ())
954
954
{
955
955
irep_idt component_name = with_expr.where ().get (ID_component_name);
956
956
if (suffix_starts_with_field (suffix, id2string (component_name)))
@@ -966,7 +966,8 @@ void value_sett::get_value_set_rec(
966
966
original_type,
967
967
ns);
968
968
}
969
- else if (to_struct_type (expr_type).has_component (component_name))
969
+ else if (ns.follow_tag (to_struct_tag_type (expr.type ()))
970
+ .has_component (component_name))
970
971
{
971
972
// Looking for a non-overwritten member, look through this expression
972
973
get_value_set_rec (
@@ -998,7 +999,7 @@ void value_sett::get_value_set_rec(
998
999
ns);
999
1000
}
1000
1001
}
1001
- else if (expr_type .id () == ID_array && !suffix.empty ())
1002
+ else if (expr. type () .id () == ID_array && !suffix.empty ())
1002
1003
{
1003
1004
std::string new_value_suffix;
1004
1005
if (has_prefix (suffix, " []" ))
@@ -1105,8 +1106,7 @@ void value_sett::get_value_set_rec(
1105
1106
1106
1107
bool found=false ;
1107
1108
1108
- const typet &op_type = ns.follow (byte_extract_expr.op ().type ());
1109
- if (op_type.id () == ID_struct)
1109
+ if (byte_extract_expr.op ().type ().id () == ID_struct_tag)
1110
1110
{
1111
1111
exprt offset = byte_extract_expr.offset ();
1112
1112
if (eval_pointer_offset (offset, ns))
@@ -1115,7 +1115,8 @@ void value_sett::get_value_set_rec(
1115
1115
const auto offset_int = numeric_cast<mp_integer>(offset);
1116
1116
const auto type_size = pointer_offset_size (expr.type (), ns);
1117
1117
1118
- const struct_typet &struct_type = to_struct_type (op_type);
1118
+ const struct_typet &struct_type =
1119
+ ns.follow_tag (to_struct_tag_type (byte_extract_expr.op ().type ()));
1119
1120
1120
1121
for (const auto &c : struct_type.components ())
1121
1122
{
@@ -1150,10 +1151,13 @@ void value_sett::get_value_set_rec(
1150
1151
}
1151
1152
}
1152
1153
1153
- if (op_type. id () == ID_union )
1154
+ if (byte_extract_expr. op (). type (). id () == ID_union_tag )
1154
1155
{
1155
1156
// just collect them all
1156
- for (const auto &c : to_union_type (op_type).components ())
1157
+ const auto &components =
1158
+ ns.follow_tag (to_union_tag_type (byte_extract_expr.op ().type ()))
1159
+ .components ();
1160
+ for (const auto &c : components)
1157
1161
{
1158
1162
const irep_idt &name = c.get_name ();
1159
1163
member_exprt member (byte_extract_expr.op (), name, c.type ());
@@ -1429,13 +1433,12 @@ void value_sett::get_reference_set_rec(
1429
1433
// We cannot introduce a cast from scalar to non-scalar,
1430
1434
// thus, we can only adjust the types of structs and unions.
1431
1435
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)
1436
+ if (
1437
+ object.type ().id () == ID_struct_tag ||
1438
+ object.type ().id () == ID_union_tag)
1436
1439
{
1437
1440
// adjust type?
1438
- if (ns. follow ( struct_op.type ())!=final_object_type )
1441
+ if (struct_op.type () != object. type () )
1439
1442
{
1440
1443
member_expr.compound () =
1441
1444
typecast_exprt (member_expr.compound (), struct_op.type ());
@@ -1478,11 +1481,10 @@ void value_sett::assign(
1478
1481
output (std::cout);
1479
1482
#endif
1480
1483
1481
- const typet &type=ns.follow (lhs.type ());
1482
-
1483
- if (type.id () == ID_struct)
1484
+ if (lhs.type ().id () == ID_struct_tag)
1484
1485
{
1485
- for (const auto &c : to_struct_type (type).components ())
1486
+ for (const auto &c :
1487
+ ns.follow_tag (to_struct_tag_type (lhs.type ())).components ())
1486
1488
{
1487
1489
const typet &subtype = c.type ();
1488
1490
const irep_idt &name = c.get_name ();
@@ -1513,12 +1515,14 @@ void value_sett::assign(
1513
1515
" rhs.type():\n " +
1514
1516
rhs.type ().pretty () + " \n " + " lhs.type():\n " + lhs.type ().pretty ());
1515
1517
1516
- const typet &followed = ns.follow (rhs.type ());
1517
-
1518
- if (followed.id () == ID_struct || followed.id () == ID_union)
1518
+ if (rhs.type ().id () == ID_struct_tag || rhs.type ().id () == ID_union_tag)
1519
1519
{
1520
1520
const struct_union_typet &rhs_struct_union_type =
1521
- to_struct_union_type (followed);
1521
+ rhs.type ().id () == ID_struct_tag
1522
+ ? static_cast <const struct_union_typet &>(
1523
+ ns.follow_tag (to_struct_tag_type (rhs.type ())))
1524
+ : static_cast <const struct_union_typet &>(
1525
+ ns.follow_tag (to_union_tag_type (rhs.type ())));
1522
1526
1523
1527
const typet &rhs_subtype = rhs_struct_union_type.component_type (name);
1524
1528
rhs_member = simplify_expr (member_exprt{rhs, name, rhs_subtype}, ns);
@@ -1528,30 +1532,30 @@ void value_sett::assign(
1528
1532
}
1529
1533
}
1530
1534
}
1531
- else if (type.id ()== ID_array)
1535
+ else if (lhs. type () .id () == ID_array)
1532
1536
{
1533
1537
const index_exprt lhs_index (
1534
1538
lhs,
1535
1539
exprt (ID_unknown, c_index_type ()),
1536
- to_array_type (type).element_type ());
1540
+ to_array_type (lhs. type () ).element_type ());
1537
1541
1538
1542
if (rhs.id ()==ID_unknown ||
1539
1543
rhs.id ()==ID_invalid)
1540
1544
{
1541
1545
assign (
1542
1546
lhs_index,
1543
- exprt (rhs.id (), to_array_type (type).element_type ()),
1547
+ exprt (rhs.id (), to_array_type (lhs. type () ).element_type ()),
1544
1548
ns,
1545
1549
is_simplified,
1546
1550
add_to_sets);
1547
1551
}
1548
1552
else
1549
1553
{
1550
1554
DATA_INVARIANT (
1551
- rhs.type () == type,
1555
+ rhs.type () == lhs. type () ,
1552
1556
" value_sett::assign types should match, got: "
1553
1557
" rhs.type():\n " +
1554
- rhs.type ().pretty () + " \n " + " type:\n " + type.pretty ());
1558
+ rhs.type ().pretty () + " \n " + " type:\n " + lhs. type () .pretty ());
1555
1559
1556
1560
if (rhs.id ()==ID_array_of)
1557
1561
{
@@ -1575,7 +1579,7 @@ void value_sett::assign(
1575
1579
const index_exprt op0_index (
1576
1580
to_with_expr (rhs).old (),
1577
1581
exprt (ID_unknown, c_index_type ()),
1578
- to_array_type (type).element_type ());
1582
+ to_array_type (lhs. type () ).element_type ());
1579
1583
1580
1584
assign (lhs_index, op0_index, ns, is_simplified, add_to_sets);
1581
1585
assign (
@@ -1586,7 +1590,7 @@ void value_sett::assign(
1586
1590
const index_exprt rhs_index (
1587
1591
rhs,
1588
1592
exprt (ID_unknown, c_index_type ()),
1589
- to_array_type (type).element_type ());
1593
+ to_array_type (lhs. type () ).element_type ());
1590
1594
assign (lhs_index, rhs_index, ns, is_simplified, true );
1591
1595
}
1592
1596
}
@@ -1683,15 +1687,15 @@ void value_sett::assign_rec(
1683
1687
{
1684
1688
const auto &lhs_member_expr = to_member_expr (lhs);
1685
1689
const auto &component_name = lhs_member_expr.get_component_name ();
1686
-
1687
- const typet &type = ns.follow (lhs_member_expr.compound ().type ());
1690
+ const exprt &compound = lhs_member_expr.compound ();
1688
1691
1689
1692
DATA_INVARIANT (
1690
- type.id () == ID_struct || type.id () == ID_union,
1693
+ compound .type ().id () == ID_struct_tag ||
1694
+ compound .type ().id () == ID_union_tag,
1691
1695
" operand 0 of member expression must be struct or union" );
1692
1696
1693
1697
assign_rec (
1694
- lhs_member_expr. compound () ,
1698
+ compound ,
1695
1699
values_rhs,
1696
1700
" ." + id2string (component_name) + suffix,
1697
1701
ns,
0 commit comments