52 goto_functionst::function_mapt::iterator f_it);
65 if(existing_symbol !=
nullptr)
79 new_symbol.
name = symbol_name;
80 new_symbol.
mode = function_symbol.
mode;
83 new_symbol.
type = return_type;
86 new_symbol.
type.
set(ID_C_no_initialization_required,
true);
99 typet return_type =
function.type.return_type();
113 function_symbol.
type =
function.type;
119 if(i_it->is_return())
122 i_it->code.operands().size() == 1,
123 "return instructions should have one operand");
129 i_it->make_assignment(assignment);
144 if(i_it->is_function_call())
150 "indirect function calls should have been removed prior to running " 157 typet old_return_type;
158 bool is_stub = function_is_stub(function_id);
174 old_return_type = return_value.
type();
197 return_value, function_call.
lhs().
type());
204 t_a->make_assignment();
205 t_a->source_location=i_it->source_location;
207 t_a->function=i_it->function;
216 t_d->source_location=i_it->source_location;
218 t_d->function=i_it->function;
231 auto function_is_stub = [&goto_functions](
const irep_idt &function_id) {
232 auto findit = goto_functions.
function_map.find(function_id);
235 "called function should have some entry in the function map");
236 return !findit->second.body_available();
253 if(goto_function.body.empty())
285 rr(goto_model_function, function_is_stub);
311 symbol_tablet::symbolst::const_iterator rv_it=
312 symbol_table.
symbols.find(rv_name);
314 if(rv_it != symbol_table.
symbols.end())
322 goto_functionst::function_mapt::iterator f_it)
324 const irep_idt function_id=f_it->first;
329 symbol_tablet::symbolst::const_iterator rv_it=
340 function_symbol.
type=f_it->second.type;
343 irep_idt rv_name_id=rv_it->second.name;
348 bool did_something =
false;
352 if(i_it->is_assign())
355 if(assign.
lhs().
id()!=ID_symbol ||
363 did_something =
true;
381 if(i_it->is_function_call())
400 goto_programt::instructionst::iterator next=i_it;
404 "non-void function call must be followed by #return_value read");
406 if(!next->is_assign())
411 if(assign.
rhs().
id()!=ID_symbol)
420 function_call.
lhs()=assign.
lhs();
426 next!=goto_program.
instructions.end() && next->is_dead(),
427 "read from #return_value should be followed by DEAD #return_value");
437 bool unmodified=
true;
void restore(goto_functionst &goto_functions)
The type of an expression, extends irept.
irep_idt name
The unique identifier.
std::function< bool(const irep_idt &)> function_is_stubt
virtual void erase(const symbolst::const_iterator &entry)=0
Remove a symbol from the symbol table.
const std::string & id2string(const irep_idt &d)
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
const irep_idt & get_function_id()
Get function id.
void undo_function_calls(goto_programt &goto_program)
turns f(...); lhs=f::return_value; into lhs=f(...)
irep_idt mode
Language mode.
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
const irep_idt & get_identifier() const
virtual symbolt * get_writeable(const irep_idt &name)=0
Find a symbol in the symbol table for read-write access.
irep_idt module
Name of module the symbol belongs to.
function_mapt function_map
typet & type()
Return the type of the expression.
symbol_tablet symbol_table
Symbol table.
code_typet original_return_type(const symbol_table_baset &symbol_table, const irep_idt &function_id)
Get code type of a function that has had remove_returns run upon it.
goto_functionst::goto_functiont & get_goto_function()
Get GOTO function.
journalling_symbol_tablet & get_symbol_table()
Get symbol table.
const code_assignt & to_code_assign(const codet &code)
const irep_idt & id() const
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
instructionst::iterator targett
const exprt & op0() const =delete
instructionst instructions
The list of instructions in the goto program.
API to expression classes.
Internally generated symbol table entryThis is a symbol generated as part of translation to or modifi...
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
::goto_functiont goto_functiont
bool restore_returns(goto_functionst::function_mapt::iterator f_it)
turns an assignment to fkt::return_value back into 'return x'
targett insert_after(const_targett target)
Insertion after the instruction pointed-to by the given instruction iterator target.
A side_effect_exprt that returns a non-deterministically chosen value.
codet representation of a function call statement.
A collection of goto functions.
void restore_returns(goto_modelt &goto_model)
restores return statements
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
remove_returnst(symbol_table_baset &_symbol_table)
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
void remove_returns(symbol_table_baset &symbol_table, goto_functionst &goto_functions)
removes returns
static exprt conditional_cast(const exprt &expr, const typet &type)
const source_locationt & source_location() const
A generic container class for the GOTO intermediate representation of one function.
symbol_table_baset & symbol_table
typet type
Type of symbol.
void replace_returns(const irep_idt &function_id, goto_functionst::goto_functiont &function)
turns 'return x' into an assignment to fkt::return_value
Base class for all expressions.
irep_idt base_name
Base (non-scoped) name.
The symbol table base class interface.
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
#define Forall_goto_functions(it, functions)
symbol_exprt get_or_create_return_value_symbol(const irep_idt &function_id)
A codet representing the removal of a local variable going out of scope.
void do_function_calls(function_is_stubt function_is_stub, goto_programt &goto_program)
turns x=f(...) into f(...); lhs=f::return_value;
#define Forall_goto_program_instructions(it, program)
Expression to hold a symbol (variable)
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
void operator()(goto_functionst &goto_functions)
#define RETURN_VALUE_SUFFIX
codet representation of a "return from a function" statement.
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
goto_functionst goto_functions
GOTO functions.
const typet & return_type() const
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
A codet representing an assignment in the program.
void set(const irep_namet &name, const irep_idt &value)
const code_function_callt & to_code_function_call(const codet &code)
Interface providing access to a single function in a GOTO model, plus its associated symbol table...