Merge pull request #5658 from tautschnig/validation-cleanup

Cleanup validation of reference_typet

Author: tautschnig

src/util/std_types.h

@@ -1556,6 +1556,19 @@ class reference_typet:public pointer_typet
   {
     set(ID_C_reference, true);
   }
+
+  static void check(
+    const typet &type,
+    const validation_modet vm = validation_modet::INVARIANT)
+  {
+    PRECONDITION(type.id() == ID_pointer);
+    const reference_typet &reference_type =
+      static_cast<const reference_typet &>(type);
+    DATA_CHECK(
+      vm, !reference_type.get(ID_width).empty(), "reference must have width");
+    DATA_CHECK(
+      vm, reference_type.get_width() > 0, "reference must have non-zero width");
+  }
 };
 
 /// 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)
   return can_cast_type<pointer_typet>(type) && type.get_bool(ID_C_reference);
 }
 
-inline void validate_type(const reference_typet &type)
-{
-  DATA_INVARIANT(!type.get(ID_width).empty(), "reference must have width");
-  DATA_INVARIANT(type.get_width() > 0, "reference must have non-zero width");
-}
-
 /// \brief Cast a typet to a \ref reference_typet
 ///
 /// This is an unchecked conversion. \a type must be known to be \ref

src/util/validate_types.cpp

@@ -46,7 +46,10 @@ void call_on_type(const typet &type, Args &&... args)
   }
   else if(type.id() == ID_pointer)
   {
-    CALL_ON_TYPE(pointer_typet);
+    if(type.get_bool(ID_C_reference))
+      CALL_ON_TYPE(reference_typet);
+    else
+      CALL_ON_TYPE(pointer_typet);
   }
   else if(type.id() == ID_c_bool)
   {