From bcc4dc4c296fd11bd62f0f262f1a105cc86f5cf0 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Fri, 11 Aug 2017 10:27:30 +0100
Subject: [PATCH] Use byte_extract_exprt constructor

---
 src/goto-symex/symex_dereference.cpp           | 15 +++++++--------
 src/pointer-analysis/dereference.cpp           |  3 ++-
 src/pointer-analysis/value_set_dereference.cpp | 12 ++++++------
 src/util/simplify_expr_struct.cpp              |  4 ++--
 4 files changed, 17 insertions(+), 17 deletions(-)

diff --git a/src/goto-symex/symex_dereference.cpp b/src/goto-symex/symex_dereference.cpp
index a7648a2e896..82bb1073db7 100644
--- a/src/goto-symex/symex_dereference.cpp
+++ b/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);
 
diff --git a/src/pointer-analysis/dereference.cpp b/src/pointer-analysis/dereference.cpp
index 6e17aa9b794..f7ba400ef78 100644
--- a/src/pointer-analysis/dereference.cpp
+++ b/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(
diff --git a/src/pointer-analysis/value_set_dereference.cpp b/src/pointer-analysis/value_set_dereference.cpp
index c29cd31fc3c..bb8ed834903 100644
--- a/src/pointer-analysis/value_set_dereference.cpp
+++ b/src/pointer-analysis/value_set_dereference.cpp
@@ -441,10 +441,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);
       }
     }
   }
@@ -852,8 +853,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;
diff --git a/src/util/simplify_expr_struct.cpp b/src/util/simplify_expr_struct.cpp
index 421d6a85744..e6195f2cb54 100644
--- a/src/util/simplify_expr_struct.cpp
+++ b/src/util/simplify_expr_struct.cpp
@@ -10,6 +10,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #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);