Skip to content

Commit

Permalink
Return original type instead of nil in original_return_type
Browse files Browse the repository at this point in the history
which is unchanged when there is no #return_value variable
  • Loading branch information
peterschrammel committed Jun 5, 2018
1 parent 29bf299 commit 32fd0c2
Show file tree
Hide file tree
Showing 2 changed files with 6 additions and 13 deletions.
2 changes: 0 additions & 2 deletions src/cbmc/symex_coverage.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -173,8 +173,6 @@ goto_program_coverage_recordt::goto_program_coverage_recordt(

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, sig_type));

Expand Down
17 changes: 6 additions & 11 deletions src/goto-programs/remove_returns.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -290,28 +290,23 @@ void remove_returns(goto_modelt &goto_model)
/// \param symbol_table: global symbol table
/// \param function_id: function to get the type of
/// \return the function's type with its `return_type()` restored to its
/// original value if a \#return_value variable exists, or nil otherwise
/// original value
code_typet original_return_type(
const symbol_table_baset &symbol_table,
const irep_idt &function_id)
{
code_typet type;
type.make_nil();
// look up the function symbol
const symbolt &function_symbol = symbol_table.lookup_ref(function_id);
code_typet type = to_code_type(function_symbol.type);

// 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
const symbolt &function_symbol=symbol_table.lookup_ref(function_id);

type=to_code_type(function_symbol.type);
type.return_type()=rv_it->second.type;
}
if(rv_it != symbol_table.symbols.end())
type.return_type() = rv_it->second.type;

return type;
}
Expand Down

0 comments on commit 32fd0c2

Please sign in to comment.