change signature of goto_symext::symex_function_call and symex_function_call_symbol

This changes the signatures of symex_function_call and
symex_function_call_symbol, which can now enforce the fact that the function
to be executed is given as symbol expression using typing.

Author: kroening

src/goto-symex/goto_symex.h

@@ -431,11 +431,11 @@ class goto_symext
   /// \param get_goto_function: The delegate to retrieve function bodies (see
   ///   \ref get_goto_functiont)
   /// \param state: Symbolic execution state for current instruction
-  /// \param code: The function call instruction
+  /// \param instruction: The function call instruction
   virtual void symex_function_call(
     const get_goto_functiont &get_goto_function,
     statet &state,
-    const code_function_callt &code);
+    const goto_programt::instructiont &instruction);
 
   /// Symbolically execute a END_FUNCTION instruction.
   /// \param state: Symbolic execution state for current instruction
@@ -445,11 +445,15 @@ class goto_symext
   /// \param get_goto_function: The delegate to retrieve function bodies (see
   ///   \ref get_goto_functiont)
   /// \param state: Symbolic execution state for current instruction
-  /// \param code: The function call instruction
+  /// \param lhs: nil or the lhs of the function call instruction
+  /// \param function: the symbol of the function to call
+  /// \param arguments: the arguments of the function call
   virtual void symex_function_call_symbol(
     const get_goto_functiont &get_goto_function,
     statet &state,
-    const code_function_callt &code);
+    const exprt &lhs,
+    const symbol_exprt &function,
+    const exprt::operandst &arguments);
 
   /// Symbolic execution of a function call by inlining.
   /// Records the call in \p target by appending a function call step and:

src/goto-symex/symex_function_call.cpp

@@ -173,23 +173,31 @@ void goto_symext::parameter_assignments(
 void goto_symext::symex_function_call(
   const get_goto_functiont &get_goto_function,
   statet &state,
-  const code_function_callt &code)
+  const goto_programt::instructiont &instruction)
 {
-  const exprt &function=code.function();
+  const exprt &function = instruction.call_function();
 
   // If at some point symex_function_call can support more
   // expression ids(), like ID_Dereference, please expand the
   // precondition appropriately.
   PRECONDITION(function.id() == ID_symbol);
-  symex_function_call_symbol(get_goto_function, state, code);
+
+  symex_function_call_symbol(
+    get_goto_function,
+    state,
+    instruction.call_lhs(),
+    to_symbol_expr(instruction.call_function()),
+    instruction.call_arguments());
 }
 
 void goto_symext::symex_function_call_symbol(
   const get_goto_functiont &get_goto_function,
   statet &state,
-  const code_function_callt &original_code)
+  const exprt &lhs,
+  const symbol_exprt &function,
+  const exprt::operandst &arguments)
 {
-  code_function_callt code = original_code;
+  code_function_callt code(lhs, function, arguments);
 
   if(code.lhs().is_not_nil())
     code.lhs() = clean_expr(std::move(code.lhs()), state, true);

src/goto-symex/symex_main.cpp

@@ -674,13 +674,7 @@ void goto_symext::execute_next_instruction(
 
   case FUNCTION_CALL:
     if(state.reachable)
-    {
-      code_function_callt call(
-        instruction.call_lhs(),
-        instruction.call_function(),
-        instruction.call_arguments());
-      symex_function_call(get_goto_function, state, call);
-    }
+      symex_function_call(get_goto_function, state, instruction);
     else
       symex_transition(state);
     break;