Skip to content

Commit 7bebe3a

Browse files
Add validation for reference_typet
A reference type without a width is still a reference type, it's just an invalid one. Rather than the cast failing, a DATA_INVARIANT should be put on this property.
1 parent cc98932 commit 7bebe3a

File tree

1 file changed

+7
-2
lines changed

1 file changed

+7
-2
lines changed

src/util/std_types.h

Lines changed: 7 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1565,8 +1565,13 @@ class reference_typet:public pointer_typet
15651565
template <>
15661566
inline bool can_cast_type<reference_typet>(const typet &type)
15671567
{
1568-
return can_cast_type<pointer_typet>(type) && type.get_bool(ID_C_reference) &&
1569-
!type.get(ID_width).empty();
1568+
return can_cast_type<pointer_typet>(type) && type.get_bool(ID_C_reference);
1569+
}
1570+
1571+
inline void validate_type(const reference_typet &type)
1572+
{
1573+
DATA_INVARIANT(!type.get(ID_width).empty(), "reference must have width");
1574+
DATA_INVARIANT(type.get_width() > 0, "reference must have non-zero width");
15701575
}
15711576

15721577
/// \brief Cast a typet to a \ref reference_typet

0 commit comments

Comments
 (0)