pointer types now have width

Author: Daniel Kroening

src/ansi-c/ansi_c_convert_type.cpp

@@ -216,6 +216,13 @@ void ansi_c_convert_typet::read_rec(const typet &type)
   {
     c_storage_spec.alias=type.subtype().get(ID_value);
   }
+  else if(type.id()==ID_pointer)
+  {
+    // pointers have a width, much like integers
+    pointer_typet tmp=to_pointer_type(type);
+    tmp.set_width(config.ansi_c.pointer_width);
+    other.push_back(tmp);
+  }
   else
     other.push_back(type);
 }

src/ansi-c/c_typecheck_type.cpp

@@ -76,7 +76,10 @@ void c_typecheck_baset::typecheck_type(typet &type)
   else if(type.id()==ID_array)
     typecheck_array_type(to_array_type(type));
   else if(type.id()==ID_pointer)
+  {
     typecheck_type(type.subtype());
+    INVARIANT(!type.get(ID_width).empty(), "pointers must have width");
+  }
   else if(type.id()==ID_struct ||
           type.id()==ID_union)
     typecheck_compound_type(to_struct_union_type(type));

src/cpp/cpp_typecheck_type.cpp

@@ -14,6 +14,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/source_location.h>
 #include <util/simplify_expr.h>
 #include <util/c_types.h>
+#include <util/config.h>
 
 #include <ansi-c/c_qualifiers.h>
 
@@ -81,6 +82,9 @@ void cpp_typecheckt::typecheck_type(typet &type)
     // the pointer might have a qualifier, but do subtype first
     typecheck_type(type.subtype());
 
+    // we add a width, much like with integers
+    to_pointer_type(type).set_width(config.ansi_c.pointer_width);
+
     // Check if it is a pointer-to-member
     if(type.find("to-member").is_not_nil())
     {

src/util/c_types.cpp

@@ -296,12 +296,12 @@ signedbv_typet pointer_diff_type()
 
 pointer_typet pointer_type(const typet &subtype)
 {
-  return pointer_typet(subtype);
+  return pointer_typet(subtype, config.ansi_c.pointer_width);
 }
 
 reference_typet reference_type(const typet &subtype)
 {
-  return reference_typet(subtype);
+  return reference_typet(subtype, config.ansi_c.pointer_width);
 }
 
 typet void_type()