Unify the remove-returns query

between goto-program/remove-return and the respective validation check.

Author: petr-bauch

src/goto-programs/remove_returns.cpp

@@ -162,10 +162,7 @@ bool remove_returnst::do_function_calls(
         to_symbol_expr(function_call.function()).get_identifier();
 
       // Do we return anything?
-      if(
-        to_code_type(function_call.function().type()).return_type() !=
-          empty_typet() &&
-        function_call.lhs().is_not_nil())
+      if(does_function_call_return(function_call))
       {
         // replace "lhs=f(...)" by
         // "f(...); lhs=f#return_value; DEAD f#return_value;"
@@ -430,3 +427,10 @@ bool is_return_value_symbol(const symbol_exprt &symbol_expr)
 {
   return is_return_value_identifier(symbol_expr.get_identifier());
 }
+
+bool does_function_call_return(const code_function_callt &function_call)
+{
+  return to_code_type(function_call.function().type()).return_type() !=
+           empty_typet() &&
+         function_call.lhs().is_not_nil();
+}

src/goto-programs/remove_returns.h

@@ -73,6 +73,7 @@ Date:   September 2009
 
 #include <functional>
 
+#include <util/std_code.h>
 #include <util/std_types.h>
 
 class goto_functionst;
@@ -111,4 +112,9 @@ bool is_return_value_identifier(const irep_idt &id);
 /// \ref return_value_symbol
 bool is_return_value_symbol(const symbol_exprt &symbol_expr);
 
+/// Check if the \p function_call returns anything
+/// \param function_call: the function call to be investigated
+/// \return true if non-void return type and non-nil lhs
+bool does_function_call_return(const code_function_callt &function_call);
+
 #endif // CPROVER_GOTO_PROGRAMS_REMOVE_RETURNS_H

src/goto-programs/validate_goto_model.cpp

@@ -14,6 +14,7 @@ Date: Oct 2018
 #include <util/invariant.h>
 
 #include "goto_functions.h"
+#include "remove_returns.h"
 
 namespace
 {
@@ -132,7 +133,7 @@ void validate_goto_modelt::check_returns_removed()
         const auto &function_call = instr.get_function_call();
         DATA_CHECK(
           vm,
-          function_call.lhs().is_nil(),
+          !does_function_call_return(function_call),
           "function call lhs return should be nil");
       }
     }