Unify the remove-returns query
between goto-program/remove-return and the respective validation check. Update the unit-test accordingly.
This commit is contained in:
parent
a88a188245
commit
16e2a14009
|
@ -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();
|
||||
}
|
||||
|
|
|
@ -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
|
||||
|
|
|
@ -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");
|
||||
}
|
||||
}
|
||||
|
|
|
@ -217,10 +217,11 @@ SCENARIO("Validation of a goto program", "[core][goto-programs][validate]")
|
|||
|
||||
WHEN("not all returns have been removed - a function call lhs is not nil")
|
||||
{
|
||||
// int h();
|
||||
symbolt h;
|
||||
h.name = "h";
|
||||
h.mode = ID_C;
|
||||
h.type = code_typet({}, empty_typet{});
|
||||
h.type = code_typet({}, signed_int_type());
|
||||
h.value = code_blockt{};
|
||||
goto_model.symbol_table.add(h);
|
||||
|
||||
|
|
Loading…
Reference in New Issue