Make get_original_name return the expression

This avoids having an input that is also an output and make the calls to
get_original_name clearer.

Author: romainbrenguier

src/goto-symex/postcondition.cpp

@@ -130,8 +130,8 @@ void postconditiont::strengthen(exprt &dest)
        SSA_step.ssa_lhs.type().id()==ID_struct)
       return;
 
-    equal_exprt equality(SSA_step.ssa_lhs, SSA_step.ssa_rhs);
-    get_original_name(equality);
+    exprt equality =
+      get_original_name(equal_exprt{SSA_step.ssa_lhs, SSA_step.ssa_rhs});
 
     if(dest.is_true())
       dest.swap(equality);
@@ -169,8 +169,7 @@ bool postconditiont::is_used(
         it!=expr_set.end();
         it++)
     {
-      exprt tmp(*it);
-      get_original_name(tmp);
+      const exprt tmp = get_original_name(*it);
       find_symbols(tmp, symbols);
     }
 

src/goto-symex/precondition.cpp

@@ -140,8 +140,7 @@ void preconditiont::compute_rec(exprt &dest)
   }
   else if(dest==SSA_step.ssa_lhs.get_original_expr())
   {
-    dest=SSA_step.ssa_rhs;
-    get_original_name(dest);
+    dest = get_original_name(SSA_step.ssa_rhs);
   }
   else
     Forall_operands(it, dest)

src/goto-symex/renaming_level.cpp

@@ -91,37 +91,42 @@ void symex_level1t::restore_from(const current_namest &other)
   }
 }
 
-void get_original_name(exprt &expr)
+exprt get_original_name(exprt expr)
 {
-  get_original_name(expr.type());
+  expr.type() = get_original_name(std::move(expr.type()));
 
   if(expr.id() == ID_symbol && expr.get_bool(ID_C_SSA_symbol))
-    expr = to_ssa_expr(expr).get_original_expr();
+    return to_ssa_expr(expr).get_original_expr();
   else
+  {
     Forall_operands(it, expr)
-      get_original_name(*it);
+      *it = get_original_name(std::move(*it));
+    return expr;
+  }
 }
 
-void get_original_name(typet &type)
+typet get_original_name(typet type)
 {
   // rename all the symbols with their last known value
 
   if(type.id() == ID_array)
   {
     auto &array_type = to_array_type(type);
-    get_original_name(array_type.subtype());
-    get_original_name(array_type.size());
+    array_type.subtype() = get_original_name(std::move(array_type.subtype()));
+    array_type.size() = get_original_name(std::move(array_type.size()));
   }
   else if(type.id() == ID_struct || type.id() == ID_union)
   {
     struct_union_typet &s_u_type = to_struct_union_type(type);
     struct_union_typet::componentst &components = s_u_type.components();
 
     for(auto &component : components)
-      get_original_name(component.type());
+      component.type() = get_original_name(std::move(component.type()));
   }
   else if(type.id() == ID_pointer)
   {
-    get_original_name(to_pointer_type(type).subtype());
+    type.subtype() =
+      get_original_name(std::move(to_pointer_type(type).subtype()));
   }
+  return type;
 }

src/goto-symex/renaming_level.h

@@ -148,9 +148,9 @@ struct symex_level2t : public symex_renaming_levelt
 };
 
 /// Undo all levels of renaming
-void get_original_name(exprt &expr);
+exprt get_original_name(exprt expr);
 
 /// Undo all levels of renaming
-void get_original_name(typet &type);
+typet get_original_name(typet type);
 
 #endif // CPROVER_GOTO_SYMEX_RENAMING_LEVEL_H

src/goto-symex/symex_assign.cpp

@@ -491,8 +491,7 @@ void goto_symext::symex_assign_symbol(
   // Temporarily add the state guard
   guard.emplace_back(state.guard.as_expr());
 
-  exprt original_lhs = l2_full_lhs;
-  get_original_name(original_lhs);
+  const exprt original_lhs = get_original_name(l2_full_lhs);
   target.assignment(
     conjunction(guard),
     l2_lhs,

src/goto-symex/symex_dereference.cpp

@@ -202,15 +202,15 @@ void goto_symext::dereference_rec(exprt &expr, statet &state, bool write)
 {
   if(expr.id()==ID_dereference)
   {
-    dereference_exprt to_check = to_dereference_expr(expr);
     bool expr_is_not_null = false;
 
     if(state.threads.size() == 1)
     {
       const irep_idt &expr_function = state.source.function_id;
       if(!expr_function.empty())
       {
-        get_original_name(to_check);
+        const dereference_exprt to_check =
+          to_dereference_expr(get_original_name(expr));
 
         expr_is_not_null = path_storage.safe_pointers.at(expr_function)
                              .is_safe_dereference(to_check, state.source.pc);