Fix pointer type

src/ansi-c/ansi_c_convert_type.cpp

@@ -216,13 +216,20 @@ 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)
+  else if(type.id()==ID_frontend_pointer)
   {
-    // pointers have a width, much like integers
-    pointer_typet tmp=to_pointer_type(type);
-    tmp.set_width(config.ansi_c.pointer_width);
+    // We turn ID_frontend_pointer to ID_pointer
+    // Pointers have a width, much like integers,
+    // which is added here.
+    typet tmp(type);
+    tmp.id(ID_pointer);
+    tmp.set(ID_width, config.ansi_c.pointer_width);
     other.push_back(tmp);
   }
+  else if(type.id()==ID_pointer)
+  {
+    UNREACHABLE;
+  }
   else
     other.push_back(type);
 }

src/ansi-c/ansi_c_declaration.cpp

@@ -98,7 +98,7 @@ typet ansi_c_declarationt::full_type(
   // this gets types that are still raw parse trees
   while(p->is_not_nil())
   {
-    if(p->id()==ID_pointer || p->id()==ID_array ||
+    if(p->id()==ID_frontend_pointer || p->id()==ID_array ||
        p->id()==ID_vector || p->id()==ID_c_bit_field ||
        p->id()==ID_block_pointer || p->id()==ID_code)
       p=&p->subtype();

src/ansi-c/c_typecheck_type.cpp

@@ -1492,19 +1492,22 @@ void c_typecheck_baset::adjust_function_parameter(typet &type) const
 {
   if(type.id()==ID_array)
   {
+    source_locationt source_location=type.source_location();
     type=pointer_type(type.subtype());
-    type.remove(ID_size);
-    type.remove(ID_C_constant);
+    type.add_source_location()=source_location;
   }
   else if(type.id()==ID_code)
   {
     // see ISO/IEC 9899:1999 page 199 clause 8,
     // may be hidden in typedef
+    source_locationt source_location=type.source_location();
     type=pointer_type(type);
+    type.add_source_location()=source_location;
   }
   else if(type.id()==ID_KnR)
   {
     // any KnR args without type yet?
     type=signed_int_type(); // the default is integer!
+    // no source location
   }
 }

src/ansi-c/parser.y

@@ -3065,7 +3065,10 @@ unary_identifier_declarator:
         {
           // the type_qualifier_list is for the pointer,
           // and not the identifier_declarator
-          stack_type($1)=pointer_type(typet(ID_abstract));
+          // The below is deliberately not using pointer_type();
+          // the width is added during conversion.
+          stack_type($1).id(ID_frontend_pointer);
+          stack_type($1).subtype()=typet(ID_abstract);
           $2=merge($2, $1); // dest=$2
           make_subtype($3, $2); // dest=$3
           $$=$3;
@@ -3249,13 +3252,19 @@ unary_abstract_declarator:
           '*'
         {
           $$=$1;
-          stack_type($$)=pointer_type(typet(ID_abstract));
+          // The below is deliberately not using pointer_type();
+          // the width is added during conversion.
+          stack_type($$).id(ID_frontend_pointer);
+          stack_type($$).subtype()=typet(ID_abstract);
         }
         | '*' attribute_type_qualifier_list
         {
           // The type_qualifier_list belongs to the pointer,
           // not to the (missing) abstract declarator.
-          stack_type($1)=pointer_type(typet(ID_abstract));
+          // The below is deliberately not using pointer_type();
+          // the width is added during conversion.
+          stack_type($1).id(ID_frontend_pointer);
+          stack_type($1).subtype()=typet(ID_abstract);
           $$=merge($2, $1);
         }
         | '*' abstract_declarator
@@ -3267,7 +3276,10 @@ unary_abstract_declarator:
         {
           // The type_qualifier_list belongs to the pointer,
           // not to the abstract declarator.
-          stack_type($1)=pointer_type(typet(ID_abstract));
+          // The below is deliberately not using pointer_type();
+          // the width is added during conversion.
+          stack_type($1).id(ID_frontend_pointer);
+          stack_type($1).subtype()=typet(ID_abstract);
           $2=merge($2, $1); // dest=$2
           make_subtype($3, $2); // dest=$3
           $$=$3;
@@ -3286,13 +3298,19 @@ parameter_unary_abstract_declarator:
           '*'
         {
           $$=$1;
-          stack_type($$)=pointer_type(typet(ID_abstract));
+          // The below is deliberately not using pointer_type();
+          // the width is added during conversion.
+          stack_type($$).id(ID_frontend_pointer);
+          stack_type($$).subtype()=typet(ID_abstract);
         }
         | '*' attribute_type_qualifier_list
         {
           // The type_qualifier_list belongs to the pointer,
           // not to the (missing) abstract declarator.
-          stack_type($1)=pointer_type(typet(ID_abstract));
+          // The below is deliberately not using pointer_type();
+          // the width is added during conversion.
+          stack_type($1).id(ID_frontend_pointer);
+          stack_type($1).subtype()=typet(ID_abstract);
           $$=merge($2, $1);
         }
         | '*' parameter_abstract_declarator
@@ -3304,7 +3322,10 @@ parameter_unary_abstract_declarator:
         {
           // The type_qualifier_list belongs to the pointer,
           // not to the (missing) abstract declarator.
-          stack_type($1)=pointer_type(typet(ID_abstract));
+          // The below is deliberately not using pointer_type();
+          // the width is added during conversion.
+          stack_type($1).id(ID_frontend_pointer);
+          stack_type($1).subtype()=typet(ID_abstract);
           $2=merge($2, $1); // dest=$2
           make_subtype($3, $2); // dest=$3
           $$=$3;

src/ansi-c/parser_static.inc

@@ -187,7 +187,7 @@ static void make_subtype(typet &dest, typet &src)
   #endif
 
   assert(src.id()==ID_array ||
-         src.id()==ID_pointer ||
+         src.id()==ID_frontend_pointer ||
          src.id()==ID_code ||
          src.id()==ID_merged_type ||
          src.id()==ID_abstract ||
@@ -207,7 +207,7 @@ static void make_subtype(typet &dest, typet &src)
       sub=&(p->subtypes().back());
     }
 
-    if(sub->id()==ID_pointer ||
+    if(sub->id()==ID_frontend_pointer ||
        sub->id()==ID_array ||
        sub->id()==ID_code)
     {
@@ -290,7 +290,10 @@ Function: make_pointer
 
 static void make_pointer(const YYSTYPE dest)
 {
-  stack_type(dest)=pointer_type(typet(ID_abstract));
+  // The below deliberately avoids pointer_type().
+  // The width is set during conversion.
+  stack_type(dest).id(ID_frontend_pointer);
+  stack_type(dest).subtype()=typet(ID_abstract);
 }
 
 /*******************************************************************\

src/cpp/cpp_convert_type.cpp

@@ -159,6 +159,19 @@ void cpp_convert_typet::read_rec(const typet &type)
     tmp.id(ID_empty);
     other.push_back(tmp);
   }
+  else if(type.id()==ID_frontend_pointer)
+  {
+    // add width and turn into ID_pointer
+    typet tmp=type;
+    tmp.id(ID_pointer);
+    tmp.set(ID_width, config.ansi_c.pointer_width);
+    other.push_back(tmp);
+  }
+  else if(type.id()==ID_pointer)
+  {
+    // ignore, we unfortunately convert multiple times
+    other.push_back(type);
+  }
   else
   {
     other.push_back(type);
@@ -549,7 +562,6 @@ void cpp_convert_plain_type(typet &type)
   if(type.id()==ID_cpp_name ||
      type.id()==ID_struct ||
      type.id()==ID_union ||
-     type.id()==ID_pointer ||
      type.id()==ID_array ||
      type.id()==ID_code ||
      type.id()==ID_unsignedbv ||

src/cpp/cpp_convert_type.h

@@ -14,6 +14,6 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/type.h>
 
-void cpp_convert_plain_type(typet &type);
+void cpp_convert_plain_type(typet &);
 
 #endif // CPROVER_CPP_CPP_CONVERT_TYPE_H

src/cpp/parse.cpp

@@ -18,9 +18,9 @@ Author: Daniel Kroening, [email protected]
 #include <util/std_code.h>
 #include <util/std_expr.h>
 #include <util/std_types.h>
-#include <util/c_types.h>
 
 #include <ansi-c/ansi_c_y.tab.h>
+#include <util/c_types.h>
 
 #include "cpp_token_buffer.h"
 #include "cpp_member_spec.h"
@@ -3016,7 +3016,7 @@ bool Parser::optPtrOperator(typet &ptrs)
 
     if(t=='*')
     {
-      typet op=pointer_type(typet(ID_nil));
+      typet op(ID_frontend_pointer); // width gets set during conversion
       cpp_tokent tk;
       lex.get_token(tk);
       set_location(op, tk);
@@ -3079,7 +3079,7 @@ bool Parser::optPtrOperator(typet &ptrs)
     {
       cpp_tokent tk;
       lex.get_token(tk);
-      typet op=pointer_type(typet(ID_nil));
+      typet op(ID_frontend_pointer); // width gets set during conversion
       op.set(ID_C_reference, true);
       set_location(op, tk);
       t_list.push_front(op);
@@ -3088,7 +3088,7 @@ bool Parser::optPtrOperator(typet &ptrs)
     {
       cpp_tokent tk;
       lex.get_token(tk);
-      typet op=pointer_type(typet(ID_nil));
+      typet op(ID_frontend_pointer); // width gets set during conversion
       op.set(ID_C_rvalue_reference, true);
       set_location(op, tk);
       t_list.push_front(op);
@@ -3531,7 +3531,7 @@ bool Parser::rPtrToMember(irept &ptr_to_mem)
   std::cout << std::string(__indent, ' ') << "Parser::rPtrToMember 0\n";
   #endif
 
-  typet ptm=pointer_type(typet(ID_nil));
+  typet ptm(ID_frontend_pointer); // width gets set during conversion
   irept &name = ptm.add("to-member");
   name=cpp_namet();
   irept::subt &components=name.get_sub();
@@ -6478,6 +6478,7 @@ bool Parser::rPrimaryExpr(exprt &exp)
 
   case TOK_NULLPTR:
     lex.get_token(tk);
+    // as an exception, we set the width of pointer
     exp=constant_exprt(ID_NULL, pointer_type(typet(ID_nullptr)));
     set_location(exp, tk);
     #ifdef DEBUG

src/util/irep_ids.def

@@ -104,6 +104,7 @@ IREP_ID_ONE(skip)
 IREP_ID_ONE(arguments)
 IREP_ID_ONE(array)
 IREP_ID_ONE(size)
+IREP_ID_ONE(frontend_pointer)
 IREP_ID_ONE(pointer)
 IREP_ID_ONE(block_pointer)
 IREP_ID_ONE(switch)