Add is_return_value_* methods

Now that RETURN_VALUE_SUFFIX is hidden, these provide a way to easily differentiate an ordinary global
variable from one introduced by remove_returns.

Author: smowton

src/goto-programs/remove_returns.cpp

@@ -14,6 +14,7 @@ Date:   September 2009
 #include "remove_returns.h"
 
 #include <util/std_expr.h>
+#include <util/suffix.h>
 
 #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());
+}

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

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 \

unit/goto-programs/remove_returns.cpp

@@ -0,0 +1,43 @@
+/*******************************************************************\
+
+Module: Unit tests for remove_returns
+
+Author: Diffblue Ltd.
+
+\*******************************************************************/
+
+#include <testing-utils/use_catch.h>
+
+#include <goto-programs/remove_returns.h>
+#include <util/namespace.h>
+#include <util/std_expr.h>
+#include <util/std_types.h>
+#include <util/symbol_table.h>
+
+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()));
+}