Merge pull request #3792 from tautschnig/deprecation-byte_extract_exprt

Construct byte_extract_exprt in a non-deprecated way

Author: Daniel Kroening

src/goto-symex/symex_other.cpp

@@ -151,22 +151,24 @@ void goto_symext::symex_other(
     // check for size (or type) mismatch and adjust
     if(!base_type_eq(dest_array.type(), src_array.type(), ns))
     {
-      byte_extract_exprt be(byte_extract_id());
-
       if(statement==ID_array_copy)
       {
-        be.op()=src_array;
-        be.offset()=from_integer(0, index_type());
-        be.type()=dest_array.type();
+        byte_extract_exprt be(
+          byte_extract_id(),
+          src_array,
+          from_integer(0, index_type()),
+          dest_array.type());
         src_array.swap(be);
         do_simplify(src_array);
       }
       else
       {
         // ID_array_replace
-        be.op()=dest_array;
-        be.offset()=from_integer(0, index_type());
-        be.type()=src_array.type();
+        byte_extract_exprt be(
+          byte_extract_id(),
+          dest_array,
+          from_integer(0, index_type()),
+          src_array.type());
         dest_array.swap(be);
         do_simplify(dest_array);
       }

src/solvers/lowering/byte_operators.cpp

@@ -411,11 +411,10 @@ static exprt lower_byte_update(
               src.id() == ID_byte_update_little_endian
                 ? ID_byte_extract_little_endian
                 : ID_byte_extract_big_endian,
+              src.value(),
+              i_expr,
               subtype);
 
-            byte_extract_expr.op() = src.value();
-            byte_extract_expr.offset()=i_expr;
-
             new_value=lower_byte_extract(byte_extract_expr, ns);
           }
 
@@ -483,11 +482,9 @@ static exprt lower_byte_update(
               src.id() == ID_byte_update_little_endian
                 ? ID_byte_extract_little_endian
                 : ID_byte_extract_big_endian,
+                src.value(), stored_value_offset,
               element_size < sub_size ? src.value().type() : subtype);
 
-            byte_extract_expr.op() = src.value();
-            byte_extract_expr.offset()=stored_value_offset;
-
             new_value=lower_byte_extract(byte_extract_expr, ns);
           }