Make function call take renamedt arguments

This reflects the assumption this makes on the expressions passed as
arguments.

Author: romainbrenguier

src/goto-symex/symex_function_call.cpp

@@ -17,6 +17,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/exception_utils.h>
 #include <util/invariant.h>
 #include <util/prefix.h>
+#include <util/range.h>
 
 static void locality(
   const irep_idt &function_identifier,
@@ -270,9 +271,10 @@ void goto_symext::symex_function_call_code(
   }
 
   // read the arguments -- before the locality renaming
-  exprt::operandst arguments = call.arguments();
-  for(auto &a : arguments)
-    a = state.rename(std::move(a), ns).get();
+  const exprt::operandst &arguments = call.arguments();
+  const std::vector<renamedt<exprt, L2>> renamed_arguments =
+    make_range(arguments).map(
+      [&](const exprt &a) { return state.rename(a, ns); });
 
   // we hide the call if the caller and callee are both hidden
   const bool callee_is_hidden = ns.lookup(identifier).is_hidden();
@@ -281,7 +283,7 @@ void goto_symext::symex_function_call_code(
 
   // record the call
   target.function_call(
-    state.guard.as_expr(), identifier, arguments, state.source, hidden);
+    state.guard.as_expr(), identifier, renamed_arguments, state.source, hidden);
 
   if(!goto_function.body_available())
   {

src/goto-symex/symex_target.h

@@ -14,6 +14,8 @@ Author: Daniel Kroening, [email protected]
 
 #include <goto-programs/goto_program.h>
 
+#include "renaming_level.h"
+
 class ssa_exprt;
 class symbol_exprt;
 
@@ -155,7 +157,7 @@ class symex_targett
   virtual void function_call(
     const exprt &guard,
     const irep_idt &function_id,
-    const std::vector<exprt> &ssa_function_arguments,
+    const std::vector<renamedt<exprt, L2>> &ssa_function_arguments,
     const sourcet &source,
     bool hidden) = 0;
 

src/goto-symex/symex_target_equation.cpp

@@ -188,7 +188,7 @@ void symex_target_equationt::location(
 void symex_target_equationt::function_call(
   const exprt &guard,
   const irep_idt &function_id,
-  const std::vector<exprt> &ssa_function_arguments,
+  const std::vector<renamedt<exprt, L2>> &function_arguments,
   const sourcet &source,
   const bool hidden)
 {
@@ -197,7 +197,8 @@ void symex_target_equationt::function_call(
 
   SSA_step.guard = guard;
   SSA_step.called_function = function_id;
-  SSA_step.ssa_function_arguments = ssa_function_arguments;
+  for(const auto &arg : function_arguments)
+    SSA_step.ssa_function_arguments.emplace_back(arg.get());
   SSA_step.hidden = hidden;
 
   merge_ireps(SSA_step);

src/goto-symex/symex_target_equation.h

@@ -26,6 +26,7 @@ Author: Daniel Kroening, [email protected]
 
 #include <solvers/prop/literal.h>
 
+#include "renaming_level.h"
 #include "ssa_step.h"
 #include "symex_target.h"
 
@@ -87,7 +88,7 @@ class symex_target_equationt:public symex_targett
   virtual void function_call(
     const exprt &guard,
     const irep_idt &function_id,
-    const std::vector<exprt> &ssa_function_arguments,
+    const std::vector<renamedt<exprt, L2>> &ssa_function_arguments,
     const sourcet &source,
     bool hidden);