32 exprt tmp(from->guard);
45 if(to->is_end_function())
73 out <<
"////\n" <<
"//// Function: " << f_it->first <<
"\n////\n\n";
75 output(f_it->second.body, f_it->first, out);
82 std::ostream &out)
const 91 assert(!working_set.empty());
121 while(!working_set.empty())
141 std::cout <<
"Visiting: " << l->function <<
" " <<
142 l->location_number <<
'\n';
158 if(l->is_function_call())
174 if(changed || !
seen(to_l))
201 const goto_functionst::function_mapt::const_iterator f_it,
207 if(!goto_function.body_available())
219 r->function=f_it->first;
220 r->location_number=0;
223 t->code.set(ID_identifier, code.
function());
224 t->function=f_it->first;
225 t->location_number=1;
230 new_data = state.
transform(
ns, t, l_next) || new_data;
235 assert(!goto_function.body.instructions.empty());
241 locationt l_begin=goto_function.body.instructions.begin();
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)
317 if(
function.operands().size()!=3)
318 throw "if takes three arguments";
334 goto_functions) || new_data;
336 else if(
function.
id()==ID_dereference)
344 for(
const auto &v : values)
346 if(v.id()==ID_object_descriptor)
351 goto_functionst::function_mapt::const_iterator it=
362 goto_functions) || new_data;
367 else if(
function.
id() == ID_null_object)
371 else if(
function.
id()==ID_member ||
function.id()==ID_index)
375 else if(
function.
id()==
"builtin-function")
381 throw "unexpected function_call argument: "+
382 function.id_string();
401 const goto_functionst::function_mapt::const_iterator it,
405 return fixedpoint(it->second.body, goto_functions);
const irept & get_nil_irep()
std::map< locationt, unsigned > statistics
exprt get_guard(locationt from, locationt to) const
const std::string & id2string(const irep_idt &d)
virtual void get_reference_set(const exprt &expr, expr_sett &expr_set)=0
std::set< locationt > seen_locations
const irep_idt & get_identifier() const
virtual void operator()(const goto_programt &goto_program)
locationt get_next(working_sett &working_set)
functions_donet functions_done
const object_descriptor_exprt & to_object_descriptor_expr(const exprt &expr)
Cast a generic exprt to an object_descriptor_exprt.
virtual bool transform(const namespacet &ns, locationt from, locationt to)=0
function_mapt function_map
bool visit(locationt l, working_sett &working_set, const goto_programt &goto_program, const goto_functionst &goto_functions)
virtual void update(const goto_programt &goto_program)
virtual statet & get_state()=0
goto_programt::const_targett locationt
The boolean constant true.
flow_insensitive_abstract_domain_baset::expr_sett expr_sett
instructionst::iterator targett
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)
instructionst instructions
The list of instructions in the goto program.
API to expression classes.
const irep_idt & get(const irep_namet &name) const
std::list< Target > get_successors(Target target) const
::goto_functiont goto_functiont
A side effect that returns a non-deterministically chosen value.
split an expression into a base object and a (byte) offset
goto_programt::const_targett locationt
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
std::vector< exprt > operandst
const source_locationt & source_location() const
A generic container class for the GOTO intermediate representation of one function.
bool seen(const locationt &l)
Flow Insensitive Static Analysis.
exprt get_return_lhs(locationt to) const
virtual void initialize(const goto_programt &)
targett add_instruction()
Adds an instruction at the end.
Base class for all expressions.
goto_programt & goto_program
#define forall_goto_functions(it, functions)
bool fixedpoint(const goto_programt &goto_program, const goto_functionst &goto_functions)
virtual void output(const goto_functionst &goto_functions, std::ostream &out)
void put_in_working_set(working_sett &working_set, locationt l)
std::priority_queue< locationt > working_sett
const code_function_callt & to_code_function_call(const codet &code)
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
virtual void output(const namespacet &, std::ostream &) const