Merge pull request #3780 from tautschnig/deprecation-with_exprt

Construct with_exprt in a non-deprecated way

Author: tautschnig

src/goto-programs/wp.cpp

@@ -166,12 +166,8 @@ void rewrite_assignment(exprt &lhs, exprt &rhs)
     irep_idt component_name=member_expr.get_component_name();
     exprt new_lhs=member_expr.struct_op();
 
-    with_exprt new_rhs;
-    new_rhs.type()=new_lhs.type();
-    new_rhs.old()=new_lhs;
-    new_rhs.where().id(ID_member_name);
+    with_exprt new_rhs(new_lhs, exprt(ID_member_name), rhs);
     new_rhs.where().set(ID_component_name, component_name);
-    new_rhs.new_value()=rhs;
 
     lhs=new_lhs;
     rhs=new_rhs;
@@ -183,11 +179,7 @@ void rewrite_assignment(exprt &lhs, exprt &rhs)
     const index_exprt index_expr=to_index_expr(lhs);
     exprt new_lhs=index_expr.array();
 
-    with_exprt new_rhs;
-    new_rhs.type()=new_lhs.type();
-    new_rhs.old()=new_lhs;
-    new_rhs.where()=index_expr.index();
-    new_rhs.new_value()=rhs;
+    with_exprt new_rhs(new_lhs, index_expr.index(), rhs);
 
     lhs=new_lhs;
     rhs=new_rhs;

src/util/expr_util.cpp

@@ -69,12 +69,12 @@ with_exprt make_with_expr(const update_exprt &src)
   const exprt::operandst &designator=src.designator();
   PRECONDITION(!designator.empty());
 
-  with_exprt result;
+  with_exprt result{exprt{}, exprt{}, exprt{}};
   exprt *dest=&result;
 
   forall_expr(it, designator)
   {
-    with_exprt tmp;
+    with_exprt tmp{exprt{}, exprt{}, exprt{}};
 
     if(it->id()==ID_index_designator)
     {