Merge pull request diffblue#2065 from tautschnig/be-constructor

Use byte_extract_exprt constructor

Author: kroening

src/goto-symex/symex_dereference.cpp

@@ -148,10 +148,8 @@ exprt goto_symext::address_arithmetic(
     object_descriptor_exprt ode;
     ode.build(expr, ns);
 
-    byte_extract_exprt be(byte_extract_id());
-    be.type()=expr.type();
-    be.op()=ode.root_object();
-    be.offset()=ode.offset();
+    const byte_extract_exprt be(
+      byte_extract_id(), ode.root_object(), ode.offset(), expr.type());
 
     // recursive call
     result=address_arithmetic(be, state, guard, keep_array);
@@ -206,10 +204,11 @@ exprt goto_symext::address_arithmetic(
 
     if(offset>0)
     {
-      byte_extract_exprt be(byte_extract_id());
-      be.type()=expr.type();
-      be.op()=to_ssa_expr(expr).get_l1_object();
-      be.offset()=from_integer(offset, index_type());
+      const byte_extract_exprt be(
+        byte_extract_id(),
+        to_ssa_expr(expr).get_l1_object(),
+        from_integer(offset, index_type()),
+        expr.type());
 
       result=address_arithmetic(be, state, guard, keep_array);
 

src/pointer-analysis/dereference.cpp

@@ -147,7 +147,8 @@ exprt dereferencet::read_object(
   }
 
   // give up and use byte_extract
-  return binary_exprt(object, byte_extract_id(), simplified_offset, dest_type);
+  return byte_extract_exprt(
+    byte_extract_id(), object, simplified_offset, dest_type);
 }
 
 exprt dereferencet::dereference_rec(

src/pointer-analysis/value_set_dereference.cpp

@@ -436,10 +436,11 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to(
       }
       else
       {
-        exprt byte_extract(byte_extract_id(), dereference_type);
-        byte_extract.copy_to_operands(
-          symbol_expr, pointer_offset(pointer_expr));
-        result.value=byte_extract;
+        result.value = byte_extract_exprt(
+          byte_extract_id(),
+          symbol_expr,
+          pointer_offset(pointer_expr),
+          dereference_type);
       }
     }
   }
@@ -847,8 +848,7 @@ bool value_set_dereferencet::memory_model_bytes(
   else
   {
     // no, use 'byte_extract'
-    result=exprt(byte_extract_id(), to_type);
-    result.copy_to_operands(value, offset);
+    result = byte_extract_exprt(byte_extract_id(), value, offset, to_type);
   }
 
   value=result;

src/util/simplify_expr_struct.cpp

@@ -10,6 +10,7 @@ Author: Daniel Kroening, [email protected]
 
 #include <cassert>
 
+#include "byte_operators.h"
 #include "expr.h"
 #include "namespace.h"
 #include "std_expr.h"
@@ -167,8 +168,7 @@ bool simplify_exprt::simplify_member(exprt &expr)
       plus_exprt final_offset(struct_offset, member_offset);
       simplify_node(final_offset);
 
-      exprt result(op.id(), expr.type());
-      result.copy_to_operands(op.op0(), final_offset);
+      byte_extract_exprt result(op.id(), op.op0(), final_offset, expr.type());
       expr.swap(result);
 
       simplify_rec(expr);