introduce return_value_identifier(...)

This encapsulates the scheme that is used to construct the identifier for
the symbol that holds the return value of a given function.

Author: Daniel Kroening

src/goto-programs/mm_io.cpp

@@ -56,7 +56,7 @@ void mm_io(
           const code_typet &ct=to_code_type(mm_io_r.type());
 
           irep_idt identifier=to_symbol_expr(mm_io_r).get_identifier();
-          irep_idt r_identifier=id2string(identifier)+RETURN_VALUE_SUFFIX;
+          irep_idt r_identifier = return_value_identifier(identifier, ns);
           symbol_exprt return_value(r_identifier, ct.return_type());
           if_exprt if_expr(integer_address(d.pointer()), return_value, d);
           if(!replace_expr(d, if_expr, a.rhs()))

src/goto-programs/remove_returns.cpp

@@ -19,6 +19,8 @@ Date:   September 2009
 
 #include "remove_skip.h"
 
+#define RETURN_VALUE_SUFFIX "#return_value"
+
 class remove_returnst
 {
 public:
@@ -61,7 +63,8 @@ class remove_returnst
 optionalt<symbol_exprt>
 remove_returnst::get_or_create_return_value_symbol(const irep_idt &function_id)
 {
-  const irep_idt symbol_name = id2string(function_id) + RETURN_VALUE_SUFFIX;
+  const namespacet ns(symbol_table);
+  const irep_idt symbol_name = return_value_identifier(function_id, ns);
   const symbolt *existing_symbol = symbol_table.lookup(symbol_name);
   if(existing_symbol != nullptr)
     return existing_symbol->symbol_expr();
@@ -292,7 +295,8 @@ bool remove_returnst::restore_returns(
   const irep_idt function_id=f_it->first;
 
   // do we have X#return_value?
-  std::string rv_name=id2string(function_id)+RETURN_VALUE_SUFFIX;
+  const namespacet ns(symbol_table);
+  auto rv_name = return_value_identifier(function_id, ns);
 
   symbol_tablet::symbolst::const_iterator rv_it=
     symbol_table.symbols.find(rv_name);
@@ -367,7 +371,7 @@ void remove_returnst::undo_function_calls(
       if(assign.rhs().id()!=ID_symbol)
         continue;
 
-      irep_idt rv_name=id2string(function_id)+RETURN_VALUE_SUFFIX;
+      irep_idt rv_name = return_value_identifier(function_id, ns);
       const symbol_exprt &rhs=to_symbol_expr(assign.rhs());
       if(rhs.get_identifier()!=rv_name)
         continue;
@@ -409,3 +413,8 @@ void restore_returns(goto_modelt &goto_model)
   remove_returnst rr(goto_model.symbol_table);
   rr.restore(goto_model.goto_functions);
 }
+
+irep_idt return_value_identifier(const irep_idt &identifier, const namespacet &)
+{
+  return id2string(identifier) + RETURN_VALUE_SUFFIX;
+}

src/goto-programs/remove_returns.h

@@ -75,12 +75,11 @@ Date:   September 2009
 
 #include <util/std_types.h>
 
-#define RETURN_VALUE_SUFFIX "#return_value"
-
 class goto_functionst;
 class goto_model_functiont;
 class goto_modelt;
 class symbol_table_baset;
+class namespacet;
 
 void remove_returns(symbol_table_baset &, goto_functionst &);
 
@@ -95,4 +94,8 @@ void restore_returns(symbol_table_baset &, goto_functionst &);
 
 void restore_returns(goto_modelt &);
 
+/// produces the identifier that is used to store the return
+/// value of the function with the given identifier
+irep_idt return_value_identifier(const irep_idt &, const namespacet &);
+
 #endif // CPROVER_GOTO_PROGRAMS_REMOVE_RETURNS_H

src/goto-programs/replace_calls.cpp

@@ -104,10 +104,8 @@ void replace_callst::operator()(
       const exprt &rhs = ca.rhs();
 
       INVARIANT(
-        rhs.id() != ID_symbol ||
-          !has_suffix(
-            id2string(to_symbol_expr(rhs).get_identifier()),
-            RETURN_VALUE_SUFFIX),
+        rhs.id() != ID_symbol || to_symbol_expr(rhs).get_identifier() !=
+                                   return_value_identifier(id, ns),
         "returns must not be removed before replacing calls");
     }