deal with return values and virtual functions

Author: Daniel Kroening

src/path-symex/path_symex.cpp

@@ -615,6 +615,7 @@ void path_symext::function_call_rec(
     thread.call_stack.back().current_function=function_identifier;
     thread.call_stack.back().return_location=thread.pc.next_loc();
     thread.call_stack.back().return_lhs=call.lhs();
+    thread.call_stack.back().return_rhs=nil_exprt();
 
     #if 0
     for(loc_reft l=function_entry_point; ; ++l)
@@ -720,9 +721,7 @@ Function: path_symext::return_from_function
 
 \*******************************************************************/
 
-void path_symext::return_from_function(
-  path_symex_statet &state,
-  const exprt &return_value)
+void path_symext::return_from_function(path_symex_statet &state)
 {
   path_symex_statet::threadt &thread=state.threads[state.get_current_thread()];
 
@@ -740,9 +739,10 @@ void path_symext::return_from_function(
     thread.pc=thread.call_stack.back().return_location;
 
     // assign the return value
-    if(return_value.is_not_nil() &&
+    if(thread.call_stack.back().return_rhs.is_not_nil() &&
        thread.call_stack.back().return_lhs.is_not_nil())
-      assign(state, thread.call_stack.back().return_lhs, return_value);
+      assign(state, thread.call_stack.back().return_lhs,
+                    thread.call_stack.back().return_rhs);
 
     // restore the local variables
     for(path_symex_statet::var_state_mapt::const_iterator
@@ -758,6 +758,30 @@ void path_symext::return_from_function(
 
 /*******************************************************************\
 
+Function: path_symext::set_return_value
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void path_symext::set_return_value(
+  path_symex_statet &state,
+  const exprt &v)
+{
+  path_symex_statet::threadt &thread=
+    state.threads[state.get_current_thread()];
+
+  // returning from very last function?
+  if(!thread.call_stack.empty())
+    thread.call_stack.back().return_rhs=v;
+}
+
+/*******************************************************************\
+
 Function: path_symext::do_goto
 
   Inputs:
@@ -892,17 +916,16 @@ void path_symext::operator()(
   case END_FUNCTION:
     // pop the call stack
     state.record_step();
-    return_from_function(state, nil_exprt());
+    return_from_function(state);
     break;
 
   case RETURN:
-    // pop the call stack
-    {
-      state.record_step();
-      exprt return_val=instruction.code.operands().size()==1?
-                       instruction.code.op0():nil_exprt();
-      return_from_function(state, return_val);
-    }
+    // sets the return value
+    state.record_step();
+
+    if(instruction.code.operands().size()==1)
+      set_return_value(state, instruction.code.op0());
+
     break;
 
   case START_THREAD:

src/path-symex/path_symex_class.h

@@ -61,9 +61,9 @@ class path_symext
     const exprt &function,
     std::list<path_symex_statet> &further_states);
 
-  void return_from_function(
-    path_symex_statet &state,
-    const exprt &return_value);
+  void return_from_function(path_symex_statet &state);
+  
+  void set_return_value(path_symex_statet &, const exprt &);
 
   void symex_malloc(
     path_symex_statet &state,

src/path-symex/path_symex_state.h

@@ -69,6 +69,7 @@ struct path_symex_statet
     irep_idt current_function;
     loc_reft return_location;
     exprt return_lhs;
+    exprt return_rhs;
     var_state_mapt saved_local_vars;
   };
 

src/symex/symex_parse_options.cpp

@@ -30,8 +30,8 @@ Author: Daniel Kroening, [email protected]
 #include <goto-programs/goto_inline.h>
 #include <goto-programs/xml_goto_trace.h>
 #include <goto-programs/remove_complex.h>
-#include <goto-programs/remove_returns.h>
 #include <goto-programs/remove_vector.h>
+#include <goto-programs/remove_virtual_functions.h>
 
 #include <analyses/goto_check.h>
 
@@ -542,7 +542,7 @@ bool symex_parse_optionst::process_goto_program(
     // remove stuff    
     remove_complex(symbol_table, goto_functions);
     remove_vector(symbol_table, goto_functions);
-    remove_returns(symbol_table, goto_functions);
+    remove_virtual_functions(symbol_table, goto_functions);
 
     // recalculate numbers, etc.
     goto_functions.update();