37 goto_functionst::function_mapt::iterator f_it);
44 goto_functionst::function_mapt::iterator f_it);
53 goto_functionst::function_mapt::iterator f_it)
55 typet return_type=f_it->second.type.return_type();
57 const irep_idt function_id=f_it->first;
65 symbol_tablet::symbolst::iterator s_it=
69 symbolt &function_symbol=s_it->second;
73 function_symbol.type=f_it->second.type;
78 new_symbol.
module=function_symbol.module;
82 new_symbol.
mode=function_symbol.mode;
83 new_symbol.
type=return_type;
90 if(goto_program.
empty())
99 assert(i_it->code.operands().size()==1);
104 lhs_expr.type()=return_type;
110 i_it->code=assignment;
123 if(i_it->is_function_call())
134 assert(function_call.
function().
id()==ID_symbol);
140 goto_functionst::function_mapt::const_iterator
145 "failed to find function `"+
id2string(function_id)+
156 if(f_it->second.body_available())
170 t_a->make_assignment();
171 t_a->source_location=i_it->source_location;
173 t_a->function=i_it->function;
178 if(f_it->second.body_available())
182 t_d->source_location=i_it->source_location;
184 t_d->function=i_it->function;
227 symbol_tablet::symbolst::const_iterator rv_it=
228 symbol_table.
symbols.find(rv_name);
230 if(rv_it!=symbol_table.
symbols.end())
233 symbol_tablet::symbolst::const_iterator s_it=
234 symbol_table.
symbols.find(function_id);
236 assert(s_it!=symbol_table.
symbols.end());
239 type.return_type()=rv_it->second.type;
247 goto_functionst::function_mapt::iterator f_it)
249 const irep_idt function_id=f_it->first;
254 symbol_tablet::symbolst::iterator rv_it=
261 symbol_tablet::symbolst::iterator s_it=
265 symbolt &function_symbol=s_it->second;
269 function_symbol.type=f_it->second.type;
272 irep_idt rv_name_id=rv_it->second.name;
279 if(i_it->is_assign())
282 if(assign.
lhs().
id()!=ID_symbol ||
293 while(!i_it->is_goto() && !i_it->is_end_function())
295 assert(i_it->is_dead());
302 assert(target->is_end_function());
306 assert(i_it->is_end_function());
311 i_it->code=return_code;
327 if(i_it->is_function_call())
346 goto_programt::instructionst::iterator next=i_it;
350 if(!next->is_assign())
355 if(assign.
rhs().
id()!=ID_symbol)
364 function_call.
lhs()=assign.
lhs();
370 assert(next->is_dead());
380 bool unmodified=
true;
void restore(goto_functionst &goto_functions)
The type of an expression.
irep_idt name
The unique identifier.
virtual bool lookup(const irep_idt &name, const symbolt *&symbol) const
const std::string & id2string(const irep_idt &d)
irep_idt mode
Language mode.
instructionst instructions
The list of instructions in the goto program.
const irep_idt & get_identifier() const
remove_returnst(symbol_tablet &_symbol_table)
symbol_tablet & symbol_table
bool empty() const
Is the program empty?
irep_idt module
Name of module the symbol belongs to.
symbol_tablet symbol_table
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
const code_assignt & to_code_assign(const codet &code)
const irep_idt & id() const
instructionst::const_iterator const_targett
void undo_function_calls(goto_functionst &goto_functions, goto_programt &goto_program)
turns f(...); lhs=f::return_value; into x=f(...)
API to expression classes.
code_typet original_return_type(const symbol_tablet &symbol_table, const irep_idt &function_id)
Internally generated symbol table entryThis is a symbol generated as part of translation to or modifi...
void do_function_calls(goto_functionst &goto_functions, goto_programt &goto_program)
turns x=f(...) into f(...); lhs=f::return_value;
bool restore_returns(goto_functionst::function_mapt::iterator f_it)
turns 'return x' into an assignment to fkt::return_value
A side effect that returns a non-deterministically chosen value.
targett insert_after(const_targett target)
Insertion after the given target.
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
function_mapt function_map
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
typet type
Type of symbol.
Base class for all expressions.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
irep_idt base_name
Base (non-scoped) name.
#define Forall_goto_functions(it, functions)
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
A removal of a local variable.
void set_identifier(const irep_idt &identifier)
void remove_returns(symbol_tablet &symbol_table, goto_functionst &goto_functions)
removes returns
#define Forall_goto_program_instructions(it, program)
Expression to hold a symbol (variable)
void operator()(goto_functionst &goto_functions)
#define RETURN_VALUE_SUFFIX
void replace_returns(goto_functionst::function_mapt::iterator f_it)
turns 'return x' into an assignment to fkt::return_value
goto_functionst goto_functions
const typet & return_type() const
const code_function_callt & to_code_function_call(const codet &code)
instructionst::iterator targett