Merge pull request #3765 from tautschnig/index-expr-constructor

Replace uses of deprecated index_exprt constructors

Author: kroening

src/ansi-c/c_typecast.cpp

@@ -720,10 +720,7 @@ void c_typecastt::do_typecast(exprt &expr, const typet &dest_type)
 
   if(src_type.id()==ID_array)
   {
-    index_exprt index;
-    index.array()=expr;
-    index.index()=from_integer(0, index_type());
-    index.type()=src_type.subtype();
+    index_exprt index(expr, from_integer(0, index_type()));
     expr = typecast_exprt::conditional_cast(address_of_exprt(index), dest_type);
     return;
   }

src/ansi-c/c_typecheck_expr.cpp

@@ -1189,10 +1189,7 @@ void c_typecheck_baset::typecheck_expr_typecast(exprt &expr)
   }
   else if(op_type.id()==ID_array)
   {
-    index_exprt index;
-    index.array()=op;
-    index.index()=from_integer(0, index_type());
-    index.type()=op_type.subtype();
+    index_exprt index(op, from_integer(0, index_type()));
     op=address_of_exprt(index);
   }
   else if(op_type.id()==ID_empty)

src/cpp/cpp_typecheck_expr.cpp

@@ -262,15 +262,9 @@ void cpp_typecheckt::typecheck_expr_trinary(if_exprt &expr)
     {
       // array-to-pointer conversion
 
-      index_exprt index1;
-      index1.array()=expr.op1();
-      index1.index()=from_integer(0, index_type());
-      index1.type()=expr.op1().type().subtype();
-
-      index_exprt index2;
-      index2.array()=expr.op2();
-      index2.index()=from_integer(0, index_type());
-      index2.type()=expr.op2().type().subtype();
+      index_exprt index1(expr.op1(), from_integer(0, index_type()));
+
+      index_exprt index2(expr.op2(), from_integer(0, index_type()));
 
       address_of_exprt addr1(index1);
       address_of_exprt addr2(index2);

src/goto-programs/string_instrumentation.cpp

@@ -425,10 +425,7 @@ void string_instrumentationt::do_format_string_read(
 
           if(arg_type.id()!=ID_pointer)
           {
-            index_exprt index;
-            index.array()=temp;
-            index.index()=from_integer(0, index_type());
-            index.type()=arg_type.subtype();
+            index_exprt index(temp, from_integer(0, index_type()));
             temp=address_of_exprt(index);
           }
 
@@ -474,10 +471,7 @@ void string_instrumentationt::do_format_string_read(
 
         if(arg_type.id()!=ID_pointer)
         {
-          index_exprt index;
-          index.array()=temp;
-          index.index()=from_integer(0, index_type());
-          index.type()=arg_type.subtype();
+          index_exprt index(temp, from_integer(0, index_type()));
           temp=address_of_exprt(index);
         }
 
@@ -911,10 +905,8 @@ void string_instrumentationt::invalidate_buffer(
     bufp=buffer;
   else
   {
-    index_exprt index;
-    index.array()=buffer;
-    index.index()=from_integer(0, index_type());
-    index.type()=buf_type.subtype();
+    index_exprt index(
+      buffer, from_integer(0, index_type()), buf_type.subtype());
     bufp=address_of_exprt(index);
   }
 

src/goto-symex/symex_builtin_functions.cpp

@@ -188,9 +188,8 @@ void goto_symext::symex_allocate(
   if(object_type.id()==ID_array)
   {
     const auto &array_type = to_array_type(object_type);
-    index_exprt index_expr(array_type.subtype());
-    index_expr.array()=value_symbol.symbol_expr();
-    index_expr.index()=from_integer(0, index_type());
+    index_exprt index_expr(
+      value_symbol.symbol_expr(), from_integer(0, index_type()));
     rhs = address_of_exprt(index_expr, pointer_type(array_type.subtype()));
   }
   else

src/solvers/flattening/boolbv_get.cpp

@@ -337,10 +337,7 @@ exprt boolbvt::bv_get_unbounded_array(const exprt &expr) const
         it1!=index_set.end();
         it1++)
     {
-      index_exprt index;
-      index.type()=type.subtype();
-      index.array()=expr;
-      index.index()=*it1;
+      index_exprt index(expr, *it1);
 
       exprt value=bv_get_cache(index);
       exprt index_value=bv_get_cache(*it1);

src/util/simplify_expr_array.cpp

@@ -88,10 +88,7 @@ bool simplify_exprt::simplify_index(exprt &expr)
 
       simplify_inequality(equality_expr);
 
-      index_exprt new_index_expr;
-      new_index_expr.type()=expr.type();
-      new_index_expr.array()=with_expr.op0();
-      new_index_expr.index()=expr.op1();
+      index_exprt new_index_expr(with_expr.op0(), expr.op1(), expr.type());
 
       simplify_index(new_index_expr); // recursive call