Add and use validation methods in unsignedbv_typet

Author: danpoe

src/util/std_types.h

@@ -1260,6 +1260,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.
@@ -1289,7 +1295,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;
 }
 
@@ -1298,7 +1304,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;
 }