Go to the documentation of this file.
42 if(to->is_end_function())
70 out <<
"////\n" <<
"//// Function: " << f_it->first <<
"\n////\n\n";
72 output(f_it->second.body, f_it->first, out);
79 std::ostream &out)
const
88 assert(!working_set.empty());
118 while(!working_set.empty())
122 if(
visit(l, working_set, goto_program, goto_functions))
138 std::cout <<
"Visiting: " << l->function <<
" " <<
139 l->location_number <<
'\n';
155 if(l->is_function_call())
171 if(changed || !
seen(to_l))
198 const goto_functionst::function_mapt::const_iterator f_it,
204 if(!goto_function.body_available())
216 r->function=f_it->first;
217 r->location_number=0;
220 t->code.set(ID_identifier, code.
function());
221 t->function=f_it->first;
222 t->location_number=1;
227 new_data = state.
transform(
ns, t, l_next) || new_data;
232 assert(!goto_function.body.instructions.empty());
238 locationt l_begin=goto_function.body.instructions.begin();
241 l_begin->function == f_it->first,
"function names have to match");
258 fixedpoint(goto_function.body, goto_functions);
265 locationt l_end=--goto_function.body.instructions.end();
267 assert(l_end->is_end_function());
272 new_data = state.
transform(
ns, l_end, l_next) || new_data;
280 const exprt &
function,
285 bool new_data =
false;
287 if(
function.
id()==ID_symbol)
299 goto_functionst::function_mapt::const_iterator it=
303 throw "failed to find function "+
id2string(identifier);
315 else if(
function.
id()==ID_if)
320 l_call, if_expr.true_case(), arguments, state, goto_functions);
324 l_call, if_expr.false_case(), arguments, state, goto_functions) ||
327 else if(
function.
id()==ID_dereference)
335 for(
const auto &v : values)
337 if(v.id()==ID_object_descriptor)
342 goto_functionst::function_mapt::const_iterator it=
353 goto_functions) || new_data;
358 else if(
function.
id() == ID_null_object)
362 else if(
function.
id()==ID_member ||
function.id()==ID_index)
366 else if(
function.
id()==
"builtin-function")
372 throw "unexpected function_call argument: "+
373 function.id_string();
392 const goto_functionst::function_mapt::const_iterator it,
396 return fixedpoint(it->second.body, goto_functions);
virtual void update(const goto_programt &goto_program)
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
virtual statet & get_state()=0
bool do_function_call(locationt l_call, const goto_functionst &goto_functions, const goto_functionst::function_mapt::const_iterator f_it, const exprt::operandst &arguments, statet &new_state)
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Split an expression into a base object and a (byte) offset.
Base class for all expressions.
bool do_function_call_rec(locationt l_call, const exprt &function, const exprt::operandst &arguments, statet &new_state, const goto_functionst &goto_functions)
recursion_sett recursion_set
std::list< Target > get_successors(Target target) const
Get control-flow successors of a given instruction.
function_mapt function_map
std::priority_queue< locationt > working_sett
exprt get_return_lhs(locationt to) const
virtual void initialize(const goto_programt &)
std::set< locationt > seen_locations
virtual void output(const namespacet &, std::ostream &) const
targett add_instruction()
Adds an instruction at the end.
typet & type()
Return the type of the expression.
codet representation of a function call statement.
virtual void get_reference_set(const exprt &expr, expr_sett &expr_set)=0
goto_programt::const_targett locationt
functions_donet functions_done
const std::string & id2string(const irep_idt &d)
const source_locationt & source_location() const
const irep_idt & get_identifier() const
exprt boolean_negate(const exprt &src)
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true
virtual void operator()(const goto_programt &goto_program)
const object_descriptor_exprt & to_object_descriptor_expr(const exprt &expr)
Cast an exprt to an object_descriptor_exprt.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const code_function_callt & to_code_function_call(const codet &code)
void put_in_working_set(working_sett &working_set, locationt l)
std::vector< exprt > operandst
bool fixedpoint(const goto_programt &goto_program, const goto_functionst &goto_functions)
virtual void output(const goto_functionst &goto_functions, std::ostream &out)
A side_effect_exprt that returns a non-deterministically chosen value.
::goto_functiont goto_functiont
instructionst instructions
The list of instructions in the goto program.
Deprecated expression utility functions.
std::map< locationt, unsigned > statistics
exprt get_guard(locationt from, locationt to) const
A collection of goto functions.
goto_programt::const_targett locationt
codet representation of a "return from a function" statement.
const irep_idt & get(const irep_namet &name) const
flow_insensitive_abstract_domain_baset::expr_sett expr_sett
A generic container class for the GOTO intermediate representation of one function.
#define forall_goto_functions(it, functions)
const irept & get_nil_irep()
bool visit(locationt l, working_sett &working_set, const goto_programt &goto_program, const goto_functionst &goto_functions)
The Boolean constant true.
bool seen(const locationt &l)
locationt get_next(working_sett &working_set)
virtual bool transform(const namespacet &ns, locationt from, locationt to)=0
instructionst::iterator targett