symex_target_equationt now has 'called_function' field

Author: Daniel Kroening

src/goto-symex/build_goto_trace.cpp

@@ -308,7 +308,7 @@ void build_goto_trace(
       goto_trace_step.format_string = SSA_step.format_string;
       goto_trace_step.io_id = SSA_step.io_id;
       goto_trace_step.formatted = SSA_step.formatted;
-      goto_trace_step.function_identifier = SSA_step.function_identifier;
+      goto_trace_step.function_identifier = SSA_step.called_function;
       goto_trace_step.function_arguments = SSA_step.converted_function_arguments;
 
       for(auto &arg : goto_trace_step.function_arguments)

src/goto-symex/symex_function_call.cpp

@@ -267,7 +267,7 @@ void goto_symext::symex_function_call_code(
     no_body(identifier);
 
     // record the return
-    target.function_return(state.guard.as_expr(), identifier, state.source);
+    target.function_return(state.guard.as_expr(), state.source);
 
     if(call.lhs().is_not_nil())
     {
@@ -358,8 +358,7 @@ void goto_symext::pop_frame(statet &state)
 void goto_symext::symex_end_of_function(statet &state)
 {
   // first record the return
-  target.function_return(
-    state.guard.as_expr(), state.source.function, state.source);
+  target.function_return(state.guard.as_expr(), state.source);
 
   // then get rid of the frame
   pop_frame(state);

src/goto-symex/symex_target.h

@@ -110,7 +110,6 @@ class symex_targett
   // record return from a function
   virtual void function_return(
     const exprt &guard,
-    const irep_idt &function_identifier,
     const sourcet &source)=0;
 
   // just record a location

src/goto-symex/symex_target_equation.cpp

@@ -219,7 +219,7 @@ void symex_target_equationt::function_call(
   SSA_step.guard = guard;
   SSA_step.type = goto_trace_stept::typet::FUNCTION_CALL;
   SSA_step.source = source;
-  SSA_step.function_identifier = function_identifier;
+  SSA_step.called_function = function_identifier;
   SSA_step.ssa_function_arguments = ssa_function_arguments;
 
   merge_ireps(SSA_step);
@@ -228,7 +228,6 @@ void symex_target_equationt::function_call(
 /// just record a location
 void symex_target_equationt::function_return(
   const exprt &guard,
-  const irep_idt &function_identifier,
   const sourcet &source)
 {
   SSA_steps.push_back(SSA_stept());
@@ -237,7 +236,6 @@ void symex_target_equationt::function_return(
   SSA_step.guard = guard;
   SSA_step.type = goto_trace_stept::typet::FUNCTION_RETURN;
   SSA_step.source = source;
-  SSA_step.function_identifier = function_identifier;
 
   merge_ireps(SSA_step);
 }

src/goto-symex/symex_target_equation.h

@@ -81,7 +81,6 @@ class symex_target_equationt:public symex_targett
   // record return from a function
   virtual void function_return(
     const exprt &guard,
-    const irep_idt &function_identifier,
     const sourcet &source);
 
   // just record a location
@@ -231,8 +230,8 @@ class symex_target_equationt:public symex_targett
     std::list<exprt> io_args;
     std::list<exprt> converted_io_args;
 
-    // for function call/return
-    irep_idt function_identifier;
+    // for function calls: the function that is called
+    irep_idt called_function;
 
     // for function calls
     std::vector<exprt> ssa_function_arguments,