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/util/c_types.cpp

@@ -295,12 +295,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()