Print the original return type in coverage report

remove_returns would cause return types that appear inconsistent to
the user.

Author: tautschnig

src/cbmc/symex_coverage.cpp

@@ -19,6 +19,7 @@ Date: March 2016
 #include <util/prefix.h>
 
 #include <goto-programs/goto_functions.h>
+#include <goto-programs/remove_returns.h>
 
 #include "symex_coverage.h"
 
@@ -157,8 +158,14 @@ goto_program_coverage_recordt::goto_program_coverage_recordt(
   //   </lines>
   // </method>
   xml.set_attribute("name", id2string(gf_it->first));
+
+  code_typet sig_type=
+    original_return_type(ns.get_symbol_table(), gf_it->first);
+  if(sig_type.is_nil())
+    sig_type=gf_it->second.type;
   xml.set_attribute("signature",
-                    from_type(ns, gf_it->first, gf_it->second.type));
+                    from_type(ns, gf_it->first, sig_type));
+
   xml.set_attribute("line-rate",
                     rate(lines_covered, lines_total));
   xml.set_attribute("branch-rate",

src/goto-programs/remove_returns.cpp

@@ -269,6 +269,46 @@ void remove_returns(goto_modelt &goto_model)
 
 /*******************************************************************\
 
+Function: original_return_type
+
+Inputs:
+
+Outputs:
+
+Purpose:
+
+\*******************************************************************/
+
+code_typet original_return_type(
+  const symbol_tablet &symbol_table,
+  const irep_idt &function_id)
+{
+  code_typet type;
+  type.make_nil();
+
+  // do we have X#return_value?
+  std::string rv_name=id2string(function_id)+RETURN_VALUE_SUFFIX;
+
+  symbol_tablet::symbolst::const_iterator rv_it=
+    symbol_table.symbols.find(rv_name);
+
+  if(rv_it!=symbol_table.symbols.end())
+  {
+    // look up the function symbol
+    symbol_tablet::symbolst::const_iterator s_it=
+      symbol_table.symbols.find(function_id);
+
+    assert(s_it!=symbol_table.symbols.end());
+
+    type=to_code_type(s_it->second.type);
+    type.return_type()=rv_it->second.type;
+  }
+
+  return type;
+}
+
+/*******************************************************************\
+
 Function: remove_returnst::restore_returns
 
 Inputs:
@@ -301,7 +341,7 @@ bool remove_returnst::restore_returns(
   symbolt &function_symbol=s_it->second;
 
   // restore the return type
-  f_it->second.type.return_type()=rv_it->second.type;
+  f_it->second.type=original_return_type(symbol_table, function_id);
   function_symbol.type=f_it->second.type;
 
   // remove the return_value symbol from the symbol_table

src/goto-programs/remove_returns.h

@@ -26,4 +26,8 @@ void remove_returns(goto_modelt &);
 // reverse the above operations
 void restore_returns(symbol_tablet &, goto_functionst &);
 
+code_typet original_return_type(
+  const symbol_tablet &symbol_table,
+  const irep_idt &function_id);
+
 #endif // CPROVER_GOTO_PROGRAMS_REMOVE_RETURNS_H