diff --git a/src/goto-programs/remove_returns.cpp b/src/goto-programs/remove_returns.cpp index 6aefd1cfeab..57d515d4865 100644 --- a/src/goto-programs/remove_returns.cpp +++ b/src/goto-programs/remove_returns.cpp @@ -14,6 +14,7 @@ Date: September 2009 #include "remove_returns.h" #include +#include #include "goto_model.h" @@ -419,3 +420,13 @@ return_value_symbol(const irep_idt &identifier, const namespacet &ns) const typet &return_type = to_code_type(function_symbol.type).return_type(); return symbol_exprt(return_value_identifier(identifier), return_type); } + +bool is_return_value_identifier(const irep_idt &id) +{ + return has_suffix(id2string(id), RETURN_VALUE_SUFFIX); +} + +bool is_return_value_symbol(const symbol_exprt &symbol_expr) +{ + return is_return_value_identifier(symbol_expr.get_identifier()); +} diff --git a/src/goto-programs/remove_returns.h b/src/goto-programs/remove_returns.h index d04b19c077c..5d990f82e60 100644 --- a/src/goto-programs/remove_returns.h +++ b/src/goto-programs/remove_returns.h @@ -103,4 +103,12 @@ irep_idt return_value_identifier(const irep_idt &); /// value of the function with the given identifier symbol_exprt return_value_symbol(const irep_idt &, const namespacet &); +/// Returns true if \p id is a special return-value symbol produced by +/// \ref return_value_identifier +bool is_return_value_identifier(const irep_idt &id); + +/// Returns true if \p symbol_expr is a special return-value symbol produced by +/// \ref return_value_symbol +bool is_return_value_symbol(const symbol_exprt &symbol_expr); + #endif // CPROVER_GOTO_PROGRAMS_REMOVE_RETURNS_H diff --git a/unit/Makefile b/unit/Makefile index fb914c8016e..46f8ad567aa 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -27,6 +27,7 @@ SRC += analyses/ai/ai.cpp \ goto-programs/goto_program_table_consistency.cpp \ goto-programs/goto_program_validate.cpp \ goto-programs/goto_trace_output.cpp \ + goto-programs/remove_returns.cpp \ goto-programs/xml_expr.cpp \ goto-symex/ssa_equation.cpp \ goto-symex/is_constant.cpp \ diff --git a/unit/goto-programs/remove_returns.cpp b/unit/goto-programs/remove_returns.cpp new file mode 100644 index 00000000000..7910bc7fdb1 --- /dev/null +++ b/unit/goto-programs/remove_returns.cpp @@ -0,0 +1,41 @@ +/*******************************************************************\ + +Module: Unit tests for remove_returns + +Author: Diffblue Ltd. + +\*******************************************************************/ + +#include + +#include +#include +#include +#include +#include + +TEST_CASE("Return-value removal", "[core][goto-programs][remove_returns]") +{ + symbol_tablet symbol_table; + symbolt function_symbol; + function_symbol.name = "a"; + function_symbol.pretty_name = "a"; + function_symbol.base_name = "a"; + function_symbol.type = code_typet({}, signedbv_typet(32)); + + symbol_table.add(function_symbol); + + namespacet ns(symbol_table); + + symbol_exprt a_rv_symbol = return_value_symbol("a", ns); + REQUIRE(is_return_value_symbol(a_rv_symbol)); + REQUIRE(is_return_value_identifier(a_rv_symbol.get_identifier())); + + irep_idt a_rv_id = return_value_identifier("a"); + + REQUIRE(is_return_value_identifier(a_rv_id)); + + symbol_exprt other_symbol("a::local", signedbv_typet(8)); + REQUIRE(!is_return_value_symbol(other_symbol)); + REQUIRE(!is_return_value_identifier(other_symbol.get_identifier())); +}