Skip to content

Add return_value_identifier function #4634

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 1 commit into from
May 9, 2019
Merged

Add return_value_identifier function #4634

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
13 changes: 7 additions & 6 deletions src/goto-programs/remove_returns.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -295,13 +295,9 @@ bool remove_returnst::restore_returns(
const irep_idt function_id=f_it->first;

// do we have X#return_value?
const namespacet ns(symbol_table);
auto rv_symbol = return_value_symbol(function_id, ns);
auto rv_name = rv_symbol.get_identifier();

auto rv_name = return_value_identifier(function_id);
symbol_tablet::symbolst::const_iterator rv_it=
symbol_table.symbols.find(rv_name);

if(rv_it==symbol_table.symbols.end())
return true;

Expand Down Expand Up @@ -411,10 +407,15 @@ void restore_returns(goto_modelt &goto_model)
rr.restore(goto_model.goto_functions);
}

irep_idt return_value_identifier(const irep_idt &identifier)
{
return id2string(identifier) + RETURN_VALUE_SUFFIX;
}

symbol_exprt
return_value_symbol(const irep_idt &identifier, const namespacet &ns)
{
const symbolt &function_symbol = ns.lookup(identifier);
const typet &return_type = to_code_type(function_symbol.type).return_type();
return symbol_exprt(id2string(identifier) + RETURN_VALUE_SUFFIX, return_type);
return symbol_exprt(return_value_identifier(identifier), return_type);
}
4 changes: 4 additions & 0 deletions src/goto-programs/remove_returns.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -95,6 +95,10 @@ 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 &);

/// produces the symbol that is used to store the return
/// value of the function with the given identifier
symbol_exprt return_value_symbol(const irep_idt &, const namespacet &);
Expand Down