clean up pointer qualifiers

Author: kroening

regression/cpp/Template_Specialisation1/main.ii

@@ -1,11 +1,14 @@
 #line 2 "main.ii"
-template<typename T> struct member_fkt_ptr { };
 
-// the two below are different
-//template<typename R, typename A> struct member_fkt_ptr<R (A::*)()> { };
-template<typename R, typename A> struct member_fkt_ptr<R (A::*)() const> { };
+template <class _Tp> struct remove_pointer;
+
+// the below are different
+template <class _Tp> struct remove_pointer       {typedef _Tp type;};
+template <class _Tp> struct remove_pointer<_Tp*> {typedef _Tp type;};
+template <class _Tp> struct remove_pointer<_Tp* const>          {typedef _Tp type;};
+template <class _Tp> struct remove_pointer<_Tp* volatile>       {typedef _Tp type;};
+template <class _Tp> struct remove_pointer<_Tp* const volatile> {typedef _Tp type;};
 
 int main()
 {
-  __CPROVER::dump_scopes;
 }

src/cpp/cpp_declarator.cpp

@@ -62,9 +62,15 @@ typet cpp_declaratort::merge_type(const typet &declaration_type) const
       t=declaration_type;
       break;
     }
+    else if(t.id()==ID_merged_type)
+    {
+      // the chain continues with the last one
+      assert(!t.subtypes().empty());
+      p=&t.subtypes().back();
+    }
     else
     {
-      assert(t.id()!="");
+      assert(t.id()!=irep_idt());
       p=&t.subtype();
     }
   }

src/cpp/cpp_type2name.cpp

@@ -115,8 +115,7 @@ std::string cpp_type2name(const typet &type)
 {
   std::string result;
 
-  if(type.get_bool(ID_C_constant) ||
-     type.get(ID_C_qualifier)==ID_const)
+  if(type.get_bool(ID_C_constant))
     result+="const_";
 
   if(type.get_bool(ID_C_restricted))

src/cpp/cpp_typecheck_constructor.cpp

@@ -270,7 +270,6 @@ void cpp_typecheckt::default_cpctor(
   parameter_tor.set(ID_name, cpp_parameter);
   parameter_tor.type()=reference_typet();
   parameter_tor.type().subtype().make_nil();
-  parameter_tor.type().add(ID_C_qualifier).make_nil();
   parameter_tor.add_source_location() = source_location;
 
   // Parameter declaration
@@ -473,7 +472,6 @@ void cpp_typecheckt::default_assignop(
 
   args_decl_declor.type().id(ID_pointer);
   args_decl_declor.type().set(ID_C_reference, true);
-  args_decl_declor.type().add(ID_C_qualifier).make_nil();
   args_decl_declor.type().subtype().make_nil();
   args_decl_declor.value().make_nil();
 }

src/cpp/cpp_typecheck_type.cpp

@@ -120,17 +120,6 @@ void cpp_typecheckt::typecheck_type(typet &type)
         }
       }
     }
-
-    // now do qualifier
-    if(type.find(ID_C_qualifier).is_not_nil())
-    {
-      typet &t=static_cast<typet &>(type.add(ID_C_qualifier));
-      cpp_convert_plain_type(t);
-      c_qualifierst q(t);
-      q.write(type);
-    }
-
-    type.remove(ID_C_qualifier);
   }
   else if(type.id()==ID_array)
   {

src/cpp/parse.cpp

@@ -343,7 +343,7 @@ class Parser
   unsigned number_of_errors;
   irep_idt current_function;
 
-  void merge_types(typet &src, typet &dest);
+  void merge_types(const typet &src, typet &dest);
 
   void set_location(irept &dest, const cpp_tokent &token)
   {
@@ -355,12 +355,22 @@ class Parser
       source_location.set_function(current_function);
   }
 
-  void make_subtype(typet &src, typet &dest)
+  void make_subtype(const typet &src, typet &dest)
   {
     typet *p=&dest;
+    
     while(p->id()!=irep_idt() && p->is_not_nil())
-      p=&p->subtype();
-    p->swap(src);
+    {
+      if(p->id()==ID_merged_type)
+      {
+        assert(!p->subtypes().empty());
+        p=&p->subtypes().back();
+      }
+      else
+        p=&p->subtype();
+    }
+    
+    *p=src;
   }
 
   unsigned int max_errors;
@@ -452,7 +462,7 @@ void Parser::make_sub_scope(const irep_idt &id, new_scopet::kindt kind)
 
 /*******************************************************************\
 
-Function:
+Function: Parser::rString
 
   Inputs:
 
@@ -472,7 +482,7 @@ bool Parser::rString(cpp_tokent &tk)
 
 /*******************************************************************\
 
-Function:
+Function: Parser::merge_types
 
   Inputs:
 
@@ -482,22 +492,22 @@ bool Parser::rString(cpp_tokent &tk)
 
 \*******************************************************************/
 
-void Parser::merge_types(typet &src, typet &dest)
+void Parser::merge_types(const typet &src, typet &dest)
 {
   if(src.is_nil()) return;
 
   if(dest.is_nil())
-    dest.swap(src);
+    dest=src;
   else
   {
     if(dest.id()!=ID_merged_type)
     {
       typet tmp(ID_merged_type);
       tmp.move_to_subtypes(dest);
-      dest.swap(tmp);
+      dest=tmp;
     }
 
-    dest.move_to_subtypes(src);
+    dest.copy_to_subtypes(src);
   }
 }
 
@@ -3428,7 +3438,7 @@ bool Parser::rDeclarator(
 
 /*******************************************************************\
 
-Function:
+Function: Parser::optPtrOperator
 
   Inputs:
 
@@ -3461,17 +3471,21 @@ bool Parser::optPtrOperator(typet &ptrs)
 
     if(t=='*')
     {
-      typet op(ID_pointer);
+      pointer_typet op;
       cpp_tokent tk;
       lex.get_token(tk);
       set_location(op, tk);
 
       typet cv;
       cv.make_nil();
-      optCvQualify(cv);
-      op.add(ID_C_qualifier).swap(cv);
-
-      t_list.push_back(op);
+      optCvQualify(cv); // the qualifier is for the pointer
+      if(cv.is_not_nil())
+      {
+        merge_types(op, cv);
+        t_list.push_back(cv);
+      }
+      else
+        t_list.push_back(op);
     }
     else if(t=='^')
     {
@@ -3483,10 +3497,14 @@ bool Parser::optPtrOperator(typet &ptrs)
 
       typet cv;
       cv.make_nil();
-      optCvQualify(cv);
-      op.add(ID_C_qualifier).swap(cv);
-
-      t_list.push_back(op);
+      optCvQualify(cv); // the qualifier is for the pointer
+      if(cv.is_not_nil())
+      {
+        merge_types(op, cv);
+        t_list.push_back(cv);
+      }
+      else
+        t_list.push_back(op);
     }
     else if(isPtrToMember(0))
     {
@@ -3496,10 +3514,14 @@ bool Parser::optPtrOperator(typet &ptrs)
 
       typet cv;
       cv.make_nil();
-      optCvQualify(cv);
-      op.add(ID_C_qualifier).swap(cv);
-
-      t_list.push_back(op);
+      optCvQualify(cv); // the qualifier is for the pointer
+      if(cv.is_not_nil())
+      {
+        merge_types(op, cv);
+        t_list.push_back(cv);
+      }
+      else
+        t_list.push_back(op);
     }
     else
       break;
@@ -3533,7 +3555,17 @@ bool Parser::optPtrOperator(typet &ptrs)
       it!=t_list.rend();
       it++)
   {
-    it->subtype().swap(ptrs);
+    if(it->id()==ID_merged_type)
+    {
+      assert(!it->subtypes().empty());
+      it->subtypes().back().subtype().swap(ptrs);
+    }
+    else
+    {
+      assert(it->is_not_nil());
+      it->subtype().swap(ptrs);
+    }
+
     ptrs.swap(*it);
   }
 
@@ -3947,7 +3979,7 @@ bool Parser::rOperatorName(irept &name)
 
 /*******************************************************************\
 
-Function:
+Function: Parser::rCastOperatorName
 
   Inputs:
 
@@ -3991,33 +4023,12 @@ bool Parser::rCastOperatorName(irept &name)
 
   if(!optPtrOperator(ptr))
     return false;
+    
+  make_subtype(type_name, ptr);
+  merge_types(cv2, ptr);
+  name = ptr;
 
-  if(ptr.is_nil())
-  {
-    name=type_name;
-    return true;
-  }
-  else
-  {
-    std::list<typet> t_list;
-    do
-    {
-      t_list.push_back(ptr);
-      typet tmp = ptr.subtype();
-      ptr = tmp;
-    }while(ptr.is_not_nil());
-
-    ptr = type_name;
-    while(!t_list.empty())
-    {
-      t_list.back().subtype() = ptr;
-      ptr = t_list.back();
-      t_list.pop_back();
-    }
-    merge_types(cv2,ptr);
-    name = ptr;
-    return true;
-  }
+  return true;
 }
 
 /*******************************************************************\
@@ -6117,6 +6128,7 @@ bool Parser::rTypeNameOrFunctionType(typet &tname)
 
     if(!optPtrOperator(tname))
       return false;
+
     return true;
   }
 

src/util/irep_ids.txt

@@ -391,7 +391,6 @@ C_volatile #volatile
 C_restricted #restricted
 C_identifier #identifier
 C_implicit #implicit
-C_qualifier #qualifier
 C_ptr32 #ptr32
 C_ptr64 #ptr64
 C_atomic #atomic