Validate data in pointer_typet in to_pointer_typet

Author: romainbrenguier

src/util/std_types.h

@@ -1417,8 +1417,9 @@ class pointer_typet:public bitvector_typet
 inline const pointer_typet &to_pointer_type(const typet &type)
 {
   PRECONDITION(type.id()==ID_pointer);
-  PRECONDITION(!type.get(ID_width).empty());
-  return static_cast<const pointer_typet &>(type);
+  const pointer_typet &ret = static_cast<const pointer_typet &>(type);
+  validate_type(ret);
+  return ret;
 }
 
 /*! \copydoc to_pointer_type(const typet &)
@@ -1427,8 +1428,9 @@ inline const pointer_typet &to_pointer_type(const typet &type)
 inline pointer_typet &to_pointer_type(typet &type)
 {
   PRECONDITION(type.id()==ID_pointer);
-  PRECONDITION(!type.get(ID_width).empty());
-  return static_cast<pointer_typet &>(type);
+  pointer_typet &ret = static_cast<pointer_typet &>(type);
+  validate_type(ret);
+  return ret;
 }
 
 template <>