File tree Expand file tree Collapse file tree 2 files changed +17
-7
lines changed Expand file tree Collapse file tree 2 files changed +17
-7
lines changed Original file line number Diff line number Diff line change @@ -1556,6 +1556,19 @@ class reference_typet:public pointer_typet
1556
1556
{
1557
1557
set (ID_C_reference, true );
1558
1558
}
1559
+
1560
+ static void check (
1561
+ const typet &type,
1562
+ const validation_modet vm = validation_modet::INVARIANT)
1563
+ {
1564
+ PRECONDITION (type.id () == ID_pointer);
1565
+ const reference_typet &reference_type =
1566
+ static_cast <const reference_typet &>(type);
1567
+ DATA_CHECK (
1568
+ vm, !reference_type.get (ID_width).empty (), " reference must have width" );
1569
+ DATA_CHECK (
1570
+ vm, reference_type.get_width () > 0 , " reference must have non-zero width" );
1571
+ }
1559
1572
};
1560
1573
1561
1574
// / Check whether a reference to a typet is a \ref reference_typet.
@@ -1567,12 +1580,6 @@ inline bool can_cast_type<reference_typet>(const typet &type)
1567
1580
return can_cast_type<pointer_typet>(type) && type.get_bool (ID_C_reference);
1568
1581
}
1569
1582
1570
- inline void validate_type (const reference_typet &type)
1571
- {
1572
- DATA_INVARIANT (!type.get (ID_width).empty (), " reference must have width" );
1573
- DATA_INVARIANT (type.get_width () > 0 , " reference must have non-zero width" );
1574
- }
1575
-
1576
1583
// / \brief Cast a typet to a \ref reference_typet
1577
1584
// /
1578
1585
// / This is an unchecked conversion. \a type must be known to be \ref
Original file line number Diff line number Diff line change @@ -46,7 +46,10 @@ void call_on_type(const typet &type, Args &&... args)
46
46
}
47
47
else if (type.id () == ID_pointer)
48
48
{
49
- CALL_ON_TYPE (pointer_typet);
49
+ if (type.get_bool (ID_C_reference))
50
+ CALL_ON_TYPE (reference_typet);
51
+ else
52
+ CALL_ON_TYPE (pointer_typet);
50
53
}
51
54
else if (type.id () == ID_c_bool)
52
55
{
You can’t perform that action at this time.
0 commit comments