address_of now needs a pointer type

Author: Daniel Kroening

src/ansi-c/ansi_c_entry_point.cpp

@@ -327,15 +327,13 @@ 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_type(char_type()));
-        address_of.copy_to_operands(index);
+        exprt address_of=address_of_exprt(index, pointer_type(char_type()));
 
         if(argv_symbol.type.subtype()!=address_of.type())
           address_of.make_typecast(argv_symbol.type.subtype());
 
         // assign argv[*] to the address of a string-object
-        exprt array_of("array_of", argv_symbol.type);
-        array_of.copy_to_operands(address_of);
+        array_of_exprt array_of(address_of, argv_symbol.type);
 
         init_code.copy_to_operands(
           code_assignt(argv_symbol.symbol_expr(), array_of));
@@ -399,17 +397,18 @@ bool ansi_c_entry_point(
 
         {
           const exprt &arg1=parameters[1];
+          const pointer_typet &pointer_type=
+            to_pointer_type(arg1.type());
 
-          exprt index_expr(ID_index, arg1.type().subtype());
-          index_expr.copy_to_operands(
+          index_exprt index_expr(
             argv_symbol.symbol_expr(),
-            from_integer(0, index_type()));
+            from_integer(0, index_type()),
+            pointer_type.subtype());
 
           // disable bounds check on that one
           index_expr.set("bounds_check", false);
 
-          op1=exprt(ID_address_of, arg1.type());
-          op1.move_to_operands(index_expr);
+          op1=address_of_exprt(index_expr, pointer_type);
         }
 
         // do we need envp?
@@ -419,13 +418,15 @@ bool ansi_c_entry_point(
           exprt &op2=operands[2];
 
           const exprt &arg2=parameters[2];
+          const pointer_typet &pointer_type=
+            to_pointer_type(arg2.type());
 
-          exprt index_expr(ID_index, arg2.type().subtype());
-          index_expr.copy_to_operands(
-            envp_symbol.symbol_expr(), from_integer(0, index_type()));
+          index_exprt index_expr(
+            envp_symbol.symbol_expr(),
+            from_integer(0, index_type()),
+            pointer_type.subtype());
 
-          op2=exprt(ID_address_of, arg2.type());
-          op2.move_to_operands(index_expr);
+          op2=address_of_exprt(index_expr, pointer_type);
         }
       }
     }

src/ansi-c/c_typecheck_expr.cpp

@@ -834,11 +834,10 @@ void c_typecheck_baset::typecheck_expr_symbol(exprt &expr)
 
     if(expr.type().id()==ID_code) // function designator
     { // special case: this is sugar for &f
-      exprt tmp(ID_address_of, pointer_type(expr.type()));
+      address_of_exprt tmp(expr, pointer_type(expr.type()));
       tmp.set("#implicit", true);
       tmp.add_source_location()=expr.source_location();
-      tmp.move_to_operands(expr);
-      expr.swap(tmp);
+      expr=tmp;
     }
   }
 }
@@ -1778,11 +1777,10 @@ void c_typecheck_baset::typecheck_expr_function_identifier(exprt &expr)
 {
   if(expr.type().id()==ID_code)
   {
-    exprt tmp(ID_address_of, pointer_type(expr.type()));
+    address_of_exprt tmp(expr, pointer_type(expr.type()));
     tmp.set(ID_C_implicit, true);
     tmp.add_source_location()=expr.source_location();
-    tmp.move_to_operands(expr);
-    expr.swap(tmp);
+    expr=tmp;
   }
 }
 

src/cpp/cpp_constructor.cpp

@@ -289,9 +289,7 @@ codet cpp_typecheckt::cpp_constructor(
     assert(tmp_this.id()==ID_address_of
            && tmp_this.op0().id()=="new_object");
 
-    exprt address_of=
-      address_of_exprt(object_tc, pointer_type(object_tc.type()));
-    tmp_this.swap(address_of);
+    tmp_this=address_of_exprt(object_tc);
 
     if(block.operands().empty())
       return to_code(initializer);

src/cpp/cpp_destructor.cpp

@@ -142,10 +142,7 @@ codet cpp_typecheckt::cpp_destructor(
     assert(tmp_this.id()==ID_address_of
            && tmp_this.op0().id()=="new_object");
 
-    exprt address_of=
-      address_of_exprt(object, pointer_type(object.type()));
-
-    tmp_this.swap(address_of);
+    tmp_this=address_of_exprt(object, pointer_type(object.type()));
 
     new_code.swap(initializer);
   }

src/cpp/cpp_typecheck_conversions.cpp

@@ -75,15 +75,11 @@ bool cpp_typecheckt::standard_conversion_array_to_pointer(
 
   index_exprt index(
     expr,
-    from_integer(0, index_type()),
-    expr.type().subtype());
+    from_integer(0, index_type()));
 
   index.set(ID_C_lvalue, true);
 
-  pointer_typet pointer=
-    pointer_type(expr.type().subtype());
-
-  new_expr=address_of_exprt(index, pointer);
+  new_expr=address_of_exprt(index);
 
   return true;
 }
@@ -98,14 +94,10 @@ bool cpp_typecheckt::standard_conversion_array_to_pointer(
 bool cpp_typecheckt::standard_conversion_function_to_pointer(
   const exprt &expr, exprt &new_expr) const
 {
-  const code_typet &func_type=to_code_type(expr.type());
-
   if(!expr.get_bool(ID_C_lvalue))
     return false;
 
-  pointer_typet pointer=pointer_type(func_type);
-
-  new_expr=address_of_exprt(expr, pointer);
+  new_expr=address_of_exprt(expr);
 
   return true;
 }
@@ -886,7 +878,7 @@ bool cpp_typecheckt::user_defined_conversion_sequence(
 
         if(subtype_typecast(from_struct, to_struct))
         {
-          exprt address=address_of_exprt(expr, pointer_type(expr.type()));
+          exprt address=address_of_exprt(expr);
 
           // simplify address
           if(expr.id()==ID_dereference)
@@ -1016,9 +1008,7 @@ 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=
-              address_of_exprt(expr, pointer_type(expr.type()));
-
+            address_of_exprt expr_pfrom(expr, pointer_type(expr.type()));
             pointer_typet pto=pointer_type(arg1_type);
 
             exprt expr_ptmp;
@@ -1441,12 +1431,11 @@ bool cpp_typecheckt::reference_binding(
       new_expr.swap(tmp);
     }
 
-    exprt tmp=
-      address_of_exprt(new_expr, pointer_type(new_expr.type()));
+    address_of_exprt tmp(new_expr, pointer_type(new_expr.type()));
     tmp.type().set(ID_C_reference, true);
     tmp.add_source_location()=new_expr.source_location();
 
-    new_expr.swap(tmp);
+    new_expr=tmp;
     return true;
   }
 
@@ -1707,10 +1696,9 @@ bool cpp_typecheckt::const_typecast(
     if(new_expr.type()!=type.subtype())
       return false;
 
-    exprt address_of(ID_address_of, type);
-    address_of.copy_to_operands(expr);
+    exprt address_of=address_of_exprt(expr, to_pointer_type(type));
     add_implicit_dereference(address_of);
-    new_expr.swap(address_of);
+    new_expr=address_of;
     return true;
   }
   else if(type.id()==ID_pointer)
@@ -1872,7 +1860,7 @@ bool cpp_typecheckt::reinterpret_typecast(
 
   if(is_reference(type) && e.get_bool(ID_C_lvalue))
   {
-    exprt tmp=address_of_exprt(e, pointer_type(e.type()));
+    exprt tmp=address_of_exprt(e);
     tmp.make_typecast(type);
     new_expr.swap(tmp);
     return true;
@@ -1936,7 +1924,7 @@ bool cpp_typecheckt::static_typecast(
           return true;
         }
 
-        exprt address_of=address_of_exprt(e, pointer_type(e.type()));
+        exprt address_of=address_of_exprt(e);
         make_ptr_typecast(address_of, type);
         new_expr.swap(address_of);
         return true;

src/cpp/cpp_typecheck_expr.cpp

@@ -2252,9 +2252,9 @@ void cpp_typecheckt::typecheck_side_effect_function_call(
       if(operand.type().id()!=ID_pointer &&
          operand.type()==argument.type().subtype())
       {
-        exprt tmp=address_of_exprt(operand, pointer_type(operand.type()));
+        address_of_exprt tmp(operand, pointer_type(operand.type()));
         tmp.add_source_location()=operand.source_location();
-        operand.swap(tmp);
+        operand=tmp;
       }
     }
   }
@@ -2666,9 +2666,7 @@ void cpp_typecheckt::convert_pmop(exprt &expr)
     else
     {
       assert(expr.op0().get_bool(ID_C_lvalue));
-      exprt address_of=
-        address_of_exprt(expr.op0(), pointer_type(expr.op0().type()));
-      expr.op0().swap(address_of);
+      expr.op0()=address_of_exprt(expr.op0());
     }
   }
 

src/goto-programs/string_instrumentation.cpp

@@ -825,12 +825,12 @@ void string_instrumentationt::do_strerror(
   }
 
   // return a pointer to some magic buffer
-  exprt index=exprt(ID_index, char_type());
-  index.copy_to_operands(
+  index_exprt index(
     symbol_buf.symbol_expr(),
-    from_integer(0, index_type()));
+    from_integer(0, index_type()),
+    char_type());
 
-  exprt ptr=address_of_exprt(index, pointer_type(char_type()));
+  address_of_exprt ptr(index);
 
   // make that zero-terminated
   {

src/goto-symex/auto_objects.cpp

@@ -66,8 +66,9 @@ void goto_symext::initialize_auto_object(
     {
       // could be NULL nondeterministically
 
-      address_of_exprt address_of_expr=
-        address_of_exprt(make_auto_object(type.subtype()));
+      address_of_exprt address_of_expr(
+        make_auto_object(type.subtype()),
+        pointer_type);
 
       if_exprt rhs(
         side_effect_expr_nondett(bool_typet()),

src/util/std_expr.cpp

@@ -13,10 +13,8 @@ Author: Daniel Kroening, [email protected]
 #include "arith_tools.h"
 #include "byte_operators.h"
 #include "c_types.h"
-#include "config.h"
 #include "namespace.h"
 #include "pointer_offset_size.h"
-
 #include "std_types.h"
 
 bool constant_exprt::value_is_zero_string() const
@@ -171,3 +169,20 @@ extractbits_exprt::extractbits_exprt(
   upper()=constant_exprt::integer_constant(_upper);
   lower()=constant_exprt::integer_constant(_lower);
 }
+
+/*******************************************************************\
+
+Function: address_of_exprt::address_of_exprt
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+address_of_exprt::address_of_exprt(const exprt &_op):
+  unary_exprt(ID_address_of, _op, pointer_type(_op.type()))
+{
+}

src/util/std_expr.h

@@ -2590,19 +2590,19 @@ inline extractbits_exprt &to_extractbits_expr(exprt &expr)
 
 /*! \brief Operator to return the address of an object
 */
-class address_of_exprt:public exprt
+class address_of_exprt:public unary_exprt
 {
 public:
-  explicit address_of_exprt(const exprt &op):
-    exprt(ID_address_of, pointer_typet(op.type()))
+  explicit address_of_exprt(const exprt &op);
+
+  address_of_exprt(const exprt &op, const pointer_typet &_type):
+    unary_exprt(ID_address_of, op, _type)
   {
-    copy_to_operands(op);
   }
 
   address_of_exprt():
-    exprt(ID_address_of, pointer_typet())
+    unary_exprt(ID_address_of, pointer_typet())
   {
-    operands().resize(1);
   }
 
   exprt &object()