use pointer_type() instead of pointer_typet()

Author: kroening

src/ansi-c/ansi_c_entry_point.cpp

@@ -327,8 +327,7 @@ bool ansi_c_entry_point(
         zero_string.type().set(ID_size, "infinity");
         exprt index(ID_index, char_type());
         index.copy_to_operands(zero_string, from_integer(0, uint_type()));
-        exprt address_of("address_of", pointer_typet());
-        address_of.type().subtype()=char_type();
+        exprt address_of("address_of", pointer_type(char_type()));
         address_of.copy_to_operands(index);
 
         if(argv_symbol.type.subtype()!=address_of.type())

src/ansi-c/c_typecheck_type.cpp

@@ -1498,9 +1498,7 @@ void c_typecheck_baset::adjust_function_parameter(typet &type) const
   {
     // see ISO/IEC 9899:1999 page 199 clause 8,
     // may be hidden in typedef
-    pointer_typet tmp;
-    tmp.subtype()=type;
-    type.swap(tmp);
+    type=pointer_type(type);
   }
   else if(type.id()==ID_KnR)
   {

src/cpp/cpp_convert_type.cpp

@@ -251,8 +251,8 @@ void cpp_convert_typet::read_function_type(const typet &type)
         // see if it's an array type
         if(final_type.id()==ID_array)
         {
-          final_type.id(ID_pointer);
-          final_type.remove(ID_size);
+          // turn into pointer type
+          final_type=pointer_type(final_type.subtype());
         }
 
         code_typet::parametert new_parameter(final_type);

src/cpp/cpp_typecheck_compound_type.cpp

@@ -16,6 +16,7 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
 #include <util/arith_tools.h>
 #include <util/simplify_expr.h>
 #include <util/std_types.h>
+#include <util/c_types.h>
 
 #include <ansi-c/c_qualifiers.h>
 
@@ -545,7 +546,7 @@ void cpp_typecheckt::typecheck_compound_declarator(
 
         // add a virtual-table pointer
         struct_typet::componentt compo;
-        compo.type()=pointer_typet(symbol_typet(vt_name));
+        compo.type()=pointer_type(symbol_typet(vt_name));
         compo.set_name(id2string(symbol.name) +"::@vtable_pointer");
         compo.set(ID_base_name, "@vtable_pointer");
         compo.set(
@@ -567,7 +568,7 @@ void cpp_typecheckt::typecheck_compound_declarator(
 
       // add an entry to the virtual table
       struct_typet::componentt vt_entry;
-      vt_entry.type()=pointer_typet(component.type());
+      vt_entry.type()=pointer_type(component.type());
       vt_entry.set_name(id2string(vtit->first)+"::"+virtual_name);
       vt_entry.set(ID_base_name, virtual_name);
       vt_entry.set(ID_pretty_name, virtual_name);
@@ -1353,7 +1354,7 @@ void cpp_typecheckt::add_this_to_method_type(
   if(has_volatile(method_qualifier))
     subtype.set(ID_C_volatile, true);
 
-  parameter.type()=pointer_typet(subtype);
+  parameter.type()=pointer_type(subtype);
 }
 
 void cpp_typecheckt::add_anonymous_members_to_scope(

src/cpp/cpp_typecheck_conversions.cpp

@@ -73,15 +73,17 @@ bool cpp_typecheckt::standard_conversion_array_to_pointer(
 {
   assert(expr.type().id()==ID_array);
 
-  exprt index(ID_index, expr.type().subtype());
-  index.copy_to_operands(expr, from_integer(0, index_type()));
+  index_exprt index(
+    expr,
+    from_integer(0, index_type()),
+    expr.type().subtype());
+
   index.set(ID_C_lvalue, true);
 
-  pointer_typet pointer;
-  pointer.subtype()=expr.type().subtype();
+  pointer_typet pointer=
+    pointer_type(expr.type().subtype());
 
-  new_expr=exprt(ID_address_of, pointer);
-  new_expr.move_to_operands(index);
+  new_expr=address_of_exprt(index, pointer);
 
   return true;
 }
@@ -101,12 +103,9 @@ bool cpp_typecheckt::standard_conversion_function_to_pointer(
   if(!expr.get_bool(ID_C_lvalue))
     return false;
 
-  pointer_typet pointer;
-  pointer.subtype()=func_type;
+  pointer_typet pointer=pointer_type(func_type);
 
-  new_expr=exprt(ID_address_of);
-  new_expr.copy_to_operands(expr);
-  new_expr.type()=pointer;
+  new_expr=address_of_exprt(expr, pointer);
 
   return true;
 }
@@ -887,16 +886,13 @@ bool cpp_typecheckt::user_defined_conversion_sequence(
 
         if(subtype_typecast(from_struct, to_struct))
         {
-          exprt address(ID_address_of, pointer_typet());
-          address.copy_to_operands(expr);
-          address.type().subtype()=expr.type();
+          exprt address=address_of_exprt(expr, pointer_type(expr.type()));
 
           // simplify address
           if(expr.id()==ID_dereference)
             address=expr.op0();
 
-          pointer_typet ptr_sub;
-          ptr_sub.subtype()=type;
+          pointer_typet ptr_sub=pointer_type(type);
           c_qualifierst qual_from;
           qual_from.read(expr.type());
           qual_from.write(ptr_sub.subtype());
@@ -1019,62 +1015,60 @@ bool cpp_typecheckt::user_defined_conversion_sequence(
           }
           else if(from_struct.is_not_nil() && arg1_struct.is_not_nil())
           {
-              // try derived-to-base conversion
-              exprt expr_pfrom(ID_address_of, pointer_typet());
-              expr_pfrom.type().subtype()=expr.type();
-              expr_pfrom.copy_to_operands(expr);
-
-              pointer_typet pto;
-              pto.subtype()=arg1_type;
-
-              exprt expr_ptmp;
-              tmp_rank=0;
-              if(standard_conversion_sequence(
-                  expr_pfrom, pto, expr_ptmp, tmp_rank))
+            // try derived-to-base conversion
+            exprt expr_pfrom=
+              address_of_exprt(expr, pointer_type(expr.type()));
+
+            pointer_typet pto=pointer_type(arg1_type);
+
+            exprt expr_ptmp;
+            tmp_rank=0;
+            if(standard_conversion_sequence(
+                expr_pfrom, pto, expr_ptmp, tmp_rank))
+            {
+              // check if it's ambiguous
+              if(found)
+                return false;
+              found=true;
+
+              rank+=tmp_rank;
+
+              // create temporary object
+              exprt expr_deref=
+                exprt(ID_dereference, expr_ptmp.type().subtype());
+              expr_deref.set(ID_C_lvalue, true);
+              expr_deref.copy_to_operands(expr_ptmp);
+              expr_deref.add_source_location()=expr.source_location();
+
+              exprt new_object("new_object", type);
+              new_object.set(ID_C_lvalue, true);
+              new_object.type().set(ID_C_constant, false);
+
+              exprt func_symb=cpp_symbol_expr(lookup(component.get(ID_name)));
+              func_symb.type()=comp_type;
               {
-                // check if it's ambiguous
-                if(found)
-                  return false;
-                found=true;
-
-                rank+=tmp_rank;
-
-                // create temporary object
-                exprt expr_deref=
-                  exprt(ID_dereference, expr_ptmp.type().subtype());
-                expr_deref.set(ID_C_lvalue, true);
-                expr_deref.copy_to_operands(expr_ptmp);
-                expr_deref.add_source_location()=expr.source_location();
-
-                exprt new_object("new_object", type);
-                new_object.set(ID_C_lvalue, true);
-                new_object.type().set(ID_C_constant, false);
-
-                exprt func_symb=cpp_symbol_expr(lookup(component.get(ID_name)));
-                func_symb.type()=comp_type;
-                {
-                  exprt tmp("already_typechecked");
-                  tmp.copy_to_operands(func_symb);
-                  func_symb.swap(func_symb);
-                }
-
-                side_effect_expr_function_callt ctor_expr;
-                ctor_expr.add_source_location()=expr.source_location();
-                ctor_expr.function().swap(func_symb);
-                ctor_expr.arguments().push_back(expr_deref);
-                typecheck_side_effect_function_call(ctor_expr);
-
-                new_expr.swap(ctor_expr);
-
-                assert(new_expr.get(ID_statement)==ID_temporary_object);
-
-                if(to.get_bool(ID_C_constant))
-                  new_expr.type().set(ID_C_constant, true);
+                exprt tmp("already_typechecked");
+                tmp.copy_to_operands(func_symb);
+                func_symb.swap(func_symb);
               }
+
+              side_effect_expr_function_callt ctor_expr;
+              ctor_expr.add_source_location()=expr.source_location();
+              ctor_expr.function().swap(func_symb);
+              ctor_expr.arguments().push_back(expr_deref);
+              typecheck_side_effect_function_call(ctor_expr);
+
+              new_expr.swap(ctor_expr);
+
+              assert(new_expr.get(ID_statement)==ID_temporary_object);
+
+              if(to.get_bool(ID_C_constant))
+                new_expr.type().set(ID_C_constant, true);
             }
           }
-          if(found)
-            return true;
+        }
+        if(found)
+          return true;
       }
   }
 
@@ -1297,9 +1291,8 @@ bool cpp_typecheckt::reference_binding(
         address_of_exprt tmp;
         tmp.add_source_location()=expr.source_location();
         tmp.object()=expr;
-        tmp.type()=pointer_typet();
+        tmp.type()=pointer_type(tmp.op0().type());
         tmp.type().set(ID_C_reference, true);
-        tmp.type().subtype()=tmp.op0().type();
         new_expr.swap(tmp);
       }
 
@@ -1427,10 +1420,9 @@ bool cpp_typecheckt::reference_binding(
   if(user_defined_conversion_sequence(arg_expr, type.subtype(), new_expr, rank))
   {
     address_of_exprt tmp;
-    tmp.type()=pointer_typet();
+    tmp.type()=pointer_type(new_expr.type());
     tmp.object()=new_expr;
     tmp.type().set(ID_C_reference, true);
-    tmp.type().subtype()= new_expr.type();
     tmp.add_source_location()=new_expr.source_location();
     new_expr.swap(tmp);
     return true;
@@ -1449,11 +1441,11 @@ bool cpp_typecheckt::reference_binding(
       new_expr.swap(tmp);
     }
 
-    exprt tmp(ID_address_of, pointer_typet());
-    tmp.copy_to_operands(new_expr);
+    exprt tmp=
+      address_of_exprt(new_expr, pointer_type(new_expr.type()));
     tmp.type().set(ID_C_reference, true);
-    tmp.type().subtype()= new_expr.type();
     tmp.add_source_location()=new_expr.source_location();
+
     new_expr.swap(tmp);
     return true;
   }
@@ -1880,9 +1872,7 @@ bool cpp_typecheckt::reinterpret_typecast(
 
   if(is_reference(type) && e.get_bool(ID_C_lvalue))
   {
-    exprt tmp(ID_address_of, pointer_typet());
-    tmp.type().subtype()=e.type();
-    tmp.copy_to_operands(e);
+    exprt tmp=address_of_exprt(e, pointer_type(e.type()));
     tmp.make_typecast(type);
     new_expr.swap(tmp);
     return true;
@@ -1946,10 +1936,8 @@ bool cpp_typecheckt::static_typecast(
           return true;
         }
 
-        exprt address_of(ID_address_of, pointer_typet());
-        address_of.type().subtype()=e.type();
-        address_of.copy_to_operands(e);
-        make_ptr_typecast(address_of , type);
+        exprt address_of=address_of_exprt(e, pointer_type(e.type()));
+        make_ptr_typecast(address_of, type);
         new_expr.swap(address_of);
         return true;
       }

src/cpp/cpp_typecheck_expr.cpp

@@ -755,7 +755,7 @@ void cpp_typecheckt::typecheck_expr_address_of(exprt &expr)
   const bool is_ref=is_reference(expr.type());
   c_typecheck_baset::typecheck_expr_address_of(expr);
   if(is_ref)
-    expr.type()=reference_typet(expr.type().subtype());
+    expr.type()=reference_type(expr.type().subtype());
 }
 
 void cpp_typecheckt::typecheck_expr_throw(exprt &expr)
@@ -808,8 +808,8 @@ void cpp_typecheckt::typecheck_expr_new(exprt &expr)
     expr.set(ID_size, to_array_type(expr.type()).size());
 
     // new actually returns a pointer, not an array
-    pointer_typet ptr_type;
-    ptr_type.subtype()=expr.type().subtype();
+    pointer_typet ptr_type=
+      pointer_type(expr.type().subtype());
     expr.type().swap(ptr_type);
   }
   else
@@ -819,8 +819,7 @@ void cpp_typecheckt::typecheck_expr_new(exprt &expr)
 
     expr.set(ID_statement, ID_cpp_new);
 
-    pointer_typet ptr_type;
-    ptr_type.subtype().swap(expr.type());
+    pointer_typet ptr_type=pointer_type(expr.type());
     expr.type().swap(ptr_type);
   }
 

src/cpp/cpp_typecheck_type.cpp

@@ -13,6 +13,7 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
 
 #include <util/source_location.h>
 #include <util/simplify_expr.h>
+#include <util/c_types.h>
 
 #include <ansi-c/c_qualifiers.h>
 
@@ -107,8 +108,7 @@ void cpp_typecheckt::typecheck_type(typet &type)
           // Add 'this' to the parameters
           exprt a0(ID_parameter);
           a0.set(ID_C_base_name, ID_this);
-          a0.type().id(ID_pointer);
-          a0.type().subtype() = class_object;
+          a0.type()=pointer_type(class_object);
           parameters.insert(parameters.begin(), a0);
         }
       }

src/cpp/cpp_typecheck_virtual_table.cpp

@@ -11,7 +11,7 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
 
 #include "cpp_typecheck.h"
 
-#include <util/std_types.h>
+#include <util/c_types.h>
 #include <util/std_expr.h>
 
 void cpp_typecheckt::do_virtual_table(const symbolt &symbol)
@@ -32,21 +32,20 @@ void cpp_typecheckt::do_virtual_table(const symbolt &symbol)
     const code_typet &code_type=to_code_type(compo.type());
     assert(code_type.parameters().size() > 0);
 
-    const pointer_typet &pointer_type =
-      static_cast<const pointer_typet&>(code_type.parameters()[0].type());
+    const pointer_typet &parameter_pointer_type=
+      to_pointer_type(code_type.parameters()[0].type());
 
-    irep_idt class_id=pointer_type.subtype().get("identifier");
+    irep_idt class_id=parameter_pointer_type.subtype().get("identifier");
 
     std::map<irep_idt, exprt> &value_map =
       vt_value_maps[class_id];
 
-
     exprt e=symbol_exprt(compo.get_name(), code_type);
 
     if(compo.get_bool("is_pure_virtual"))
     {
-      pointer_typet pointer_type(code_type);
-      e=null_pointer_exprt(pointer_type);
+      pointer_typet code_pointer_type=pointer_type(code_type);
+      e=null_pointer_exprt(code_pointer_type);
       value_map[compo.get("virtual_name")]=e;
     }
     else

src/cpp/parse.cpp

@@ -6476,7 +6476,7 @@ bool Parser::rPrimaryExpr(exprt &exp)
 
   case TOK_NULLPTR:
     lex.get_token(tk);
-    exp=constant_exprt(ID_NULL, pointer_typet(typet(ID_nullptr)));
+    exp=constant_exprt(ID_NULL, typet(ID_pointer, typet(ID_nullptr)));
     set_location(exp, tk);
     #ifdef DEBUG
     std::cout << std::string(__indent, ' ') << "Parser::rPrimaryExpr 6\n";