introduced ID_frontend_pointer

Author: Daniel Kroening

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/parser.y

@@ -3067,7 +3067,7 @@ unary_identifier_declarator:
           // and not the identifier_declarator
           // The below is deliberately not using pointer_type();
           // the width is added during conversion.
-          stack_type($1).id(ID_pointer);
+          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
@@ -3254,7 +3254,7 @@ unary_abstract_declarator:
           $$=$1;
           // The below is deliberately not using pointer_type();
           // the width is added during conversion.
-          stack_type($$).id(ID_pointer);
+          stack_type($$).id(ID_frontend_pointer);
           stack_type($$).subtype()=typet(ID_abstract);
         }
         | '*' attribute_type_qualifier_list
@@ -3263,7 +3263,7 @@ unary_abstract_declarator:
           // not to the (missing) abstract declarator.
           // The below is deliberately not using pointer_type();
           // the width is added during conversion.
-          stack_type($1).id(ID_pointer);
+          stack_type($1).id(ID_frontend_pointer);
           stack_type($1).subtype()=typet(ID_abstract);
           $$=merge($2, $1);
         }
@@ -3278,7 +3278,7 @@ unary_abstract_declarator:
           // not to the abstract declarator.
           // The below is deliberately not using pointer_type();
           // the width is added during conversion.
-          stack_type($1).id(ID_pointer);
+          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
@@ -3300,7 +3300,7 @@ parameter_unary_abstract_declarator:
           $$=$1;
           // The below is deliberately not using pointer_type();
           // the width is added during conversion.
-          stack_type($$).id(ID_pointer);
+          stack_type($$).id(ID_frontend_pointer);
           stack_type($$).subtype()=typet(ID_abstract);
         }
         | '*' attribute_type_qualifier_list
@@ -3309,7 +3309,7 @@ parameter_unary_abstract_declarator:
           // not to the (missing) abstract declarator.
           // The below is deliberately not using pointer_type();
           // the width is added during conversion.
-          stack_type($1).id(ID_pointer);
+          stack_type($1).id(ID_frontend_pointer);
           stack_type($1).subtype()=typet(ID_abstract);
           $$=merge($2, $1);
         }
@@ -3324,7 +3324,7 @@ parameter_unary_abstract_declarator:
           // not to the (missing) abstract declarator.
           // The below is deliberately not using pointer_type();
           // the width is added during conversion.
-          stack_type($1).id(ID_pointer);
+          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

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)
     {
@@ -292,7 +292,7 @@ static void make_pointer(const YYSTYPE dest)
 {
   // The below deliberately avoids pointer_type().
   // The width is set during conversion.
-  stack_type(dest).id(ID_pointer);
+  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

@@ -20,6 +20,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/std_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"
@@ -3015,7 +3016,7 @@ bool Parser::optPtrOperator(typet &ptrs)
 
     if(t=='*')
     {
-      typet op(ID_pointer); // width gets set during conversion
+      typet op(ID_frontend_pointer); // width gets set during conversion
       cpp_tokent tk;
       lex.get_token(tk);
       set_location(op, tk);
@@ -3078,7 +3079,7 @@ bool Parser::optPtrOperator(typet &ptrs)
     {
       cpp_tokent tk;
       lex.get_token(tk);
-      typet op(ID_pointer); // width gets set during conversion
+      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);
@@ -3087,7 +3088,7 @@ bool Parser::optPtrOperator(typet &ptrs)
     {
       cpp_tokent tk;
       lex.get_token(tk);
-      typet op(ID_pointer); // width gets set during conversion
+      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);
@@ -3530,7 +3531,7 @@ bool Parser::rPtrToMember(irept &ptr_to_mem)
   std::cout << std::string(__indent, ' ') << "Parser::rPtrToMember 0\n";
   #endif
 
-  typet ptm(ID_pointer); // width gets set during conversion
+  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();
@@ -6477,8 +6478,8 @@ bool Parser::rPrimaryExpr(exprt &exp)
 
   case TOK_NULLPTR:
     lex.get_token(tk);
-    // width of pointer gets done during conversion
-    exp=constant_exprt(ID_NULL, typet(ID_pointer, typet(ID_nullptr)));
+    // 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
     std::cout << std::string(__indent, ' ') << "Parser::rPrimaryExpr 6\n";

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)