Add and use validation methods in unsignedbv_typet

Author: danpoe

src/util/std_types.h

@@ -1245,6 +1245,12 @@ class unsignedbv_typet:public bitvector_typet
   constant_exprt smallest_expr() const;
   constant_exprt zero_expr() const;
   constant_exprt largest_expr() const;
+
+  void check(const validation_modet vm = validation_modet::INVARIANT) const
+  {
+    DATA_CHECK(
+      !get(ID_width).empty(), "unsigned bitvector type must have width");
+  }
 };
 
 /// Check whether a reference to a typet is a \ref unsignedbv_typet.
@@ -1256,12 +1262,6 @@ inline bool can_cast_type<unsignedbv_typet>(const typet &type)
   return type.id() == ID_unsignedbv;
 }
 
-inline void validate_type(const unsignedbv_typet &type)
-{
-  DATA_INVARIANT(
-    !type.get(ID_width).empty(), "unsigned bitvector type must have width");
-}
-
 /// \brief Cast a typet to an \ref unsignedbv_typet
 ///
 /// This is an unchecked conversion. \a type must be known to be \ref
@@ -1274,7 +1274,7 @@ inline const unsignedbv_typet &to_unsignedbv_type(const typet &type)
 {
   PRECONDITION(can_cast_type<unsignedbv_typet>(type));
   const unsignedbv_typet &ret = static_cast<const unsignedbv_typet &>(type);
-  validate_type(ret);
+  ret.check();
   return ret;
 }
 
@@ -1283,7 +1283,7 @@ inline unsignedbv_typet &to_unsignedbv_type(typet &type)
 {
   PRECONDITION(can_cast_type<unsignedbv_typet>(type));
   unsignedbv_typet &ret = static_cast<unsignedbv_typet &>(type);
-  validate_type(ret);
+  ret.check();
   return ret;
 }