Skip to content

Commit 32fd0c2

Browse files
Return original type instead of nil in original_return_type
which is unchanged when there is no #return_value variable
1 parent 29bf299 commit 32fd0c2

File tree

2 files changed

+6
-13
lines changed

2 files changed

+6
-13
lines changed

src/cbmc/symex_coverage.cpp

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -173,8 +173,6 @@ goto_program_coverage_recordt::goto_program_coverage_recordt(
173173

174174
code_typet sig_type=
175175
original_return_type(ns.get_symbol_table(), gf_it->first);
176-
if(sig_type.is_nil())
177-
sig_type=gf_it->second.type;
178176
xml.set_attribute("signature",
179177
from_type(ns, gf_it->first, sig_type));
180178

src/goto-programs/remove_returns.cpp

Lines changed: 6 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -290,28 +290,23 @@ void remove_returns(goto_modelt &goto_model)
290290
/// \param symbol_table: global symbol table
291291
/// \param function_id: function to get the type of
292292
/// \return the function's type with its `return_type()` restored to its
293-
/// original value if a \#return_value variable exists, or nil otherwise
293+
/// original value
294294
code_typet original_return_type(
295295
const symbol_table_baset &symbol_table,
296296
const irep_idt &function_id)
297297
{
298-
code_typet type;
299-
type.make_nil();
298+
// look up the function symbol
299+
const symbolt &function_symbol = symbol_table.lookup_ref(function_id);
300+
code_typet type = to_code_type(function_symbol.type);
300301

301302
// do we have X#return_value?
302303
std::string rv_name=id2string(function_id)+RETURN_VALUE_SUFFIX;
303304

304305
symbol_tablet::symbolst::const_iterator rv_it=
305306
symbol_table.symbols.find(rv_name);
306307

307-
if(rv_it!=symbol_table.symbols.end())
308-
{
309-
// look up the function symbol
310-
const symbolt &function_symbol=symbol_table.lookup_ref(function_id);
311-
312-
type=to_code_type(function_symbol.type);
313-
type.return_type()=rv_it->second.type;
314-
}
308+
if(rv_it != symbol_table.symbols.end())
309+
type.return_type() = rv_it->second.type;
315310

316311
return type;
317312
}

0 commit comments

Comments
 (0)