use pointer_type() instead of pointer_typet()

Author: Daniel Kroening

src/cpp/cpp_typecheck_compound_type.cpp

@@ -11,6 +11,7 @@ Author: Daniel Kroening, [email protected]
 #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>
 
@@ -601,7 +602,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(
@@ -623,7 +624,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);
@@ -1492,7 +1493,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);
 }
 
 /*******************************************************************\

src/cpp/cpp_typecheck_expr.cpp

@@ -872,7 +872,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());
 }
 
 /*******************************************************************\

src/cpp/cpp_typecheck_virtual_table.cpp

@@ -6,7 +6,7 @@ Author: Daniel Kroening, [email protected]
 
 \*******************************************************************/
 
-#include <util/std_types.h>
+#include <util/c_types.h>
 #include <util/std_expr.h>
 
 #include "cpp_typecheck.h"
@@ -37,21 +37,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

@@ -7660,7 +7660,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";

src/goto-instrument/function.cpp

@@ -41,7 +41,7 @@ code_function_callt function_to_call(
   if(s_it==symbol_table.symbols.end())
   {
     // not there
-    pointer_typet p(char_type());
+    typet p=pointer_type(char_type());
     p.subtype().set(ID_C_constant, true);
 
     code_typet function_type;

src/goto-instrument/goto_program2code.cpp

@@ -480,7 +480,7 @@ goto_programt::const_targett goto_program2codet::convert_assign_varargs(
       static_cast<typet const&>(r.find(ID_C_va_arg_type));
 
     dereference_exprt deref(
-      null_pointer_exprt(pointer_typet(va_arg_type)),
+      null_pointer_exprt(pointer_type(va_arg_type)),
       va_arg_type);
 
     type_of.arguments().push_back(deref);
@@ -1634,7 +1634,7 @@ goto_programt::const_targett goto_program2codet::convert_start_thread(
     // we don't bother setting the type
     f.lhs()=cf.lhs();
     f.function()=symbol_exprt("pthread_create", code_typet());
-    exprt n=null_pointer_exprt(pointer_typet(empty_typet()));
+    exprt n=null_pointer_exprt(pointer_type(empty_typet()));
     f.arguments().push_back(n);
     f.arguments().push_back(n);
     f.arguments().push_back(cf.function());

src/goto-instrument/thread_instrumentation.cpp

@@ -67,7 +67,7 @@ void thread_exit_instrumentation(goto_programt &goto_program)
   binary_exprt get_may("get_may");
 
   // NULL is any
-  get_may.op0()=null_pointer_exprt(to_pointer_type(pointer_type(empty_typet())));
+  get_may.op0()=null_pointer_exprt(pointer_type(empty_typet()));
   get_may.op1()=address_of_exprt(mutex_locked_string);
 
   end->make_assertion(not_exprt(get_may));

src/goto-instrument/wmm/shared_buffers.cpp

@@ -6,6 +6,8 @@ Author: Daniel Kroening, [email protected]
 
 \*******************************************************************/
 
+#include <util/c_types.h>
+
 #include "shared_buffers.h"
 #include "fence.h"
 
@@ -74,7 +76,7 @@ const shared_bufferst::varst &shared_bufferst::operator()(
       object,
       symbol.base_name,
       "$read_delayed_var",
-      pointer_typet(symbol.type));
+      pointer_type(symbol.type));
 
   for(unsigned cnt=0; cnt<nb_threads; cnt++)
   {
@@ -162,7 +164,7 @@ void shared_bufferst::add_initialization(goto_programt &goto_program)
     assignment(goto_program, t, source_location, vars.second.read_delayed,
       false_exprt());
     assignment(goto_program, t, source_location, vars.second.read_delayed_var,
-      null_pointer_exprt(pointer_typet(vars.second.type)));
+      null_pointer_exprt(pointer_type(vars.second.type)));
 
     for(const auto &id : vars.second.r_buff0_thds)
       assignment(goto_program, t, source_location, id, false_exprt());
@@ -1328,7 +1330,7 @@ void shared_bufferst::cfg_visitort::weak_memory(
                     r_it->second.object, vars.type);
                   symbol_exprt new_read_expr=symbol_exprt(
                     vars.read_delayed_var,
-                  pointer_typet(vars.type));
+                    pointer_type(vars.type));
                   symbol_exprt read_delayed_expr=symbol_exprt(
                     vars.read_delayed, bool_typet());
 

src/goto-programs/builtin_functions.cpp

@@ -728,7 +728,7 @@ void goto_convertt::do_java_new(
   // we produce a malloc side-effect, which stays
   side_effect_exprt malloc_expr(ID_malloc);
   malloc_expr.copy_to_operands(object_size);
-  malloc_expr.type()=pointer_typet(object_type);
+  malloc_expr.type()=rhs.type();
 
   goto_programt::targett t_n=dest.add_instruction(ASSIGN);
   t_n->code=code_assignt(lhs, malloc_expr);
@@ -796,7 +796,7 @@ void goto_convertt::do_java_new_array(
   // we produce a malloc side-effect, which stays
   side_effect_exprt malloc_expr(ID_malloc);
   malloc_expr.copy_to_operands(object_size);
-  malloc_expr.type()=pointer_typet(object_type);
+  malloc_expr.type()=rhs.type();
 
   goto_programt::targett t_n=dest.add_instruction(ASSIGN);
   t_n->code=code_assignt(lhs, malloc_expr);

src/goto-programs/class_identifier.cpp

@@ -9,6 +9,7 @@ Author: Chris Smowton, [email protected]
 #include "class_identifier.h"
 
 #include <util/std_expr.h>
+#include <util/c_types.h>
 #include <util/namespace.h>
 
 /*******************************************************************\
@@ -83,7 +84,7 @@ exprt get_class_identifier_field(
          "Non-pointer this-arg in remove-virtuals?");
   const auto &points_to=this_expr.type().subtype();
   if(points_to==empty_typet())
-    this_expr=typecast_exprt(this_expr, pointer_typet(suggested_type));
+    this_expr=typecast_exprt(this_expr, pointer_type(suggested_type));
   exprt deref=dereference_exprt(this_expr, this_expr.type().subtype());
   return build_class_identifier(deref, ns);
 }

src/goto-programs/remove_asm.cpp

@@ -12,6 +12,7 @@ Date:   December 2014
 #include <sstream>
 
 #include <util/std_expr.h>
+#include <util/c_types.h>
 
 #include <ansi-c/string_constant.h>
 #include <assembler/assembler_parser.h>
@@ -70,7 +71,8 @@ void remove_asmt::gcc_asm_function_call(
   code_function_callt function_call;
   function_call.lhs().make_nil();
 
-  const pointer_typet void_pointer=pointer_typet(void_typet());
+  const typet void_pointer=
+    pointer_type(void_typet());
 
   // outputs
   forall_operands(it, code.op1())

src/goto-programs/remove_exceptions.cpp

@@ -16,6 +16,7 @@ Date:   December 2016
 #include <algorithm>
 
 #include <util/std_expr.h>
+#include <util/c_types.h>
 #include <util/symbol_table.h>
 
 #include "remove_exceptions.h"
@@ -116,12 +117,12 @@ void remove_exceptionst::add_exceptional_returns(
     new_symbol.base_name=id2string(function_symbol.base_name)+EXC_SUFFIX;
     new_symbol.name=id2string(function_symbol.name)+EXC_SUFFIX;
     new_symbol.mode=function_symbol.mode;
-    new_symbol.type=pointer_typet(empty_typet());
+    new_symbol.type=pointer_type(empty_typet());
     symbol_table.add(new_symbol);
 
     // initialize the exceptional return with NULL
     symbol_exprt lhs_expr_null=new_symbol.symbol_expr();
-    null_pointer_exprt rhs_expr_null((pointer_typet(empty_typet())));
+    null_pointer_exprt rhs_expr_null(pointer_type(empty_typet()));
     goto_programt::targett t_null=
       goto_program.insert_before(goto_program.instructions.begin());
     t_null->make_assignment();
@@ -165,7 +166,7 @@ void remove_exceptionst::instrument_exception_handler(
       symbol_table.lookup(id2string(function_id)+EXC_SUFFIX);
     // next we reset the exceptional return to NULL
     symbol_exprt lhs_expr_null=function_symbol.symbol_expr();
-    null_pointer_exprt rhs_expr_null((pointer_typet(empty_typet())));
+    null_pointer_exprt rhs_expr_null(pointer_type(empty_typet()));
 
     // add the assignment
     goto_programt::targett t_null=goto_program.insert_after(instr_it);
@@ -367,7 +368,7 @@ void remove_exceptionst::instrument_function_call(
     // add a null check (so that instanceof can be applied)
     equal_exprt eq_null(
       callee_exc,
-      null_pointer_exprt(pointer_typet(empty_typet())));
+      null_pointer_exprt(pointer_type(empty_typet())));
     goto_programt::targett t_null=goto_program.insert_after(instr_it);
     t_null->make_goto(next_it);
     t_null->source_location=instr_it->source_location;

src/goto-programs/remove_virtual_functions.cpp

@@ -8,6 +8,7 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/prefix.h>
 #include <util/type_eq.h>
+#include <util/c_types.h>
 
 #include "class_hierarchy.h"
 #include "class_identifier.h"
@@ -175,7 +176,8 @@ void remove_virtual_functionst::remove_virtual_function(
         t1->make_function_call(code);
         auto &newcall=to_code_function_call(t1->code);
         newcall.function()=fun.symbol_expr;
-        pointer_typet need_type(symbol_typet(fun.symbol_expr.get(ID_C_class)));
+        typet need_type=
+          pointer_type(symbol_typet(fun.symbol_expr.get(ID_C_class)));
         if(!type_eq(newcall.arguments()[0].type(), need_type, ns))
           newcall.arguments()[0].make_typecast(need_type);
       }

src/goto-programs/string_abstraction.cpp

@@ -322,7 +322,7 @@ void string_abstractiont::add_argument(
     const irep_idt &identifier)
 {
   typet final_type=is_ptr_argument(type)?
-    type:pointer_typet(type);
+                   type:pointer_type(type);
 
   str_args.push_back(code_typet::parametert(final_type));
   str_args.back().add_source_location()=fct_symbol.location;
@@ -963,7 +963,7 @@ const typet &string_abstractiont::build_abstraction_type_rec(const typet &type,
     // char* or void* or char[]
     if(is_char_type(eff_type.subtype()) ||
         eff_type.subtype().id()==ID_empty)
-      map_entry.first->second=pointer_typet(string_struct);
+      map_entry.first->second=pointer_type(string_struct);
     else
     {
       const typet &subt=build_abstraction_type_rec(eff_type.subtype(), known);
@@ -973,8 +973,7 @@ const typet &string_abstractiont::build_abstraction_type_rec(const typet &type,
           map_entry.first->second=
             array_typet(subt, to_array_type(eff_type).size());
         else
-          map_entry.first->second=
-            pointer_typet(subt);
+          map_entry.first->second=pointer_type(subt);
       }
     }
   }

src/goto-symex/symex_builtin_functions.cpp

@@ -177,7 +177,7 @@ void goto_symext::symex_malloc(
 
   if(object_type.id()==ID_array)
   {
-    rhs.type()=pointer_typet(value_symbol.type.subtype());
+    rhs.type()=pointer_type(value_symbol.type.subtype());
     index_exprt index_expr(value_symbol.type.subtype());
     index_expr.array()=value_symbol.symbol_expr();
     index_expr.index()=from_integer(0, index_type());
@@ -186,7 +186,7 @@ void goto_symext::symex_malloc(
   else
   {
     rhs.op0()=value_symbol.symbol_expr();
-    rhs.type()=pointer_typet(value_symbol.type);
+    rhs.type()=pointer_type(value_symbol.type);
   }
 
   if(rhs.type()!=lhs.type())
@@ -496,7 +496,7 @@ void goto_symext::symex_cpp_new(
 
   // make symbol expression
 
-  exprt rhs(ID_address_of, pointer_typet());
+  exprt rhs(ID_address_of, code.type());
   rhs.type().subtype()=code.type().subtype();
 
   if(do_array)

src/goto-symex/symex_dereference.cpp

@@ -153,7 +153,7 @@ exprt goto_symext::address_arithmetic(
     }
 
     // do (expr.type() *)(((char *)op)+offset)
-    result=typecast_exprt(result, pointer_typet(char_type()));
+    result=typecast_exprt(result, pointer_type(char_type()));
 
     // there could be further dereferencing in the offset
     exprt offset=be.offset();
@@ -163,14 +163,14 @@ exprt goto_symext::address_arithmetic(
 
     // treat &array as &array[0]
     const typet &expr_type=ns.follow(expr.type());
-    pointer_typet dest_type;
+    typet dest_type_subtype;
 
     if(expr_type.id()==ID_array && !keep_array)
-      dest_type.subtype()=expr_type.subtype();
+      dest_type_subtype=expr_type.subtype();
     else
-      dest_type.subtype()=expr_type;
+      dest_type_subtype=expr_type;
 
-    result=typecast_exprt(result, dest_type);
+    result=typecast_exprt(result, pointer_type(dest_type_subtype));
   }
   else if(expr.id()==ID_index ||
           expr.id()==ID_member)
@@ -253,7 +253,7 @@ exprt goto_symext::address_arithmetic(
 
   const typet &expr_type=ns.follow(expr.type());
   assert((expr_type.id()==ID_array && !keep_array) ||
-         base_type_eq(pointer_typet(expr_type), result.type(), ns));
+         base_type_eq(pointer_type(expr_type), result.type(), ns));
 
   return result;
 }
@@ -324,7 +324,7 @@ void goto_symext::dereference_rec(
     index_exprt index_expr=to_index_expr(expr);
 
     address_of_exprt address_of_expr(index_expr.array());
-    address_of_expr.type()=pointer_typet(expr.type());
+    address_of_expr.type()=pointer_type(expr.type());
 
     dereference_exprt tmp;
     tmp.pointer()=plus_exprt(address_of_expr, index_expr.index());
@@ -361,7 +361,7 @@ void goto_symext::dereference_rec(
        to_address_of_expr(tc_op).object().type().id()==ID_array &&
        base_type_eq(
          expr.type(),
-         pointer_typet(to_address_of_expr(tc_op).object().type().subtype()),
+         pointer_type(to_address_of_expr(tc_op).object().type().subtype()),
          ns))
     {
       expr=