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