Add can_cast_type, validate_type for pointer_typet

Author: romainbrenguier

src/util/std_types.h

@@ -20,6 +20,7 @@ Author: Daniel Kroening, [email protected]
 #include "expr.h"
 #include "mp_arith.h"
 #include "invariant.h"
+#include "expr_cast.h"
 
 class constant_exprt;
 
@@ -1430,6 +1431,18 @@ inline pointer_typet &to_pointer_type(typet &type)
   return static_cast<pointer_typet &>(type);
 }
 
+template <>
+inline bool can_cast_type<pointer_typet>(const typet &type)
+{
+  return type.id() == ID_pointer;
+}
+
+inline void validate_type(const pointer_typet &type)
+{
+  DATA_INVARIANT(!type.get(ID_width).empty(), "pointer must have width");
+  DATA_INVARIANT(type.get_width() > 0, "pointer must have non-zero width");
+}
+
 /*! \brief The reference type
 */
 class reference_typet:public pointer_typet