32 exprt tmp(from->guard);
46 if(to->is_end_function())
50 assert(to->is_function_call());
62 fixedpoint(goto_functions);
70 fixedpoint(goto_program, goto_functions);
79 out <<
"////\n" <<
"//// Function: " << f_it->first <<
"\n////\n\n";
81 output(f_it->second.body, f_it->first, out);
88 std::ostream &out)
const 90 get_state().output(ns, out);
97 assert(!working_set.empty());
127 while(!working_set.empty())
131 if(visit(l, working_set, goto_program, goto_functions))
147 std::cout <<
"Visiting: " << l->function <<
" " <<
148 l->location_number <<
'\n';
151 seen_locations.insert(l);
152 if(statistics.find(l)==statistics.end())
164 if(l->is_function_call())
171 do_function_call_rec(
179 changed = get_state().transform(ns, l, to_l);
181 if(changed || !seen(to_l))
184 put_in_working_set(working_set, to_l);
208 const goto_functionst::function_mapt::const_iterator f_it,
226 r->function=f_it->first;
227 r->location_number=0;
230 t->code.set(ID_identifier, code.
function());
231 t->function=f_it->first;
232 t->location_number=1;
235 bool new_data=state.
transform(ns, l_call, r);
236 new_data = state.
transform(ns, r, t) || new_data;
237 new_data = state.
transform(ns, t, l_next) || new_data;
242 assert(!goto_function.
body.instructions.empty());
251 new_data=state.
transform(ns, l_call, l_begin);
254 if(functions_done.find(f_it->first)==
255 functions_done.end())
258 functions_done.insert(f_it->first);
265 fixedpoint(goto_function.
body, goto_functions);
274 assert(l_end->is_end_function());
279 new_data = state.
transform(ns, l_end, l_next) || new_data;
287 const exprt &
function,
292 bool new_data =
false;
294 if(
function.
id()==ID_symbol)
296 const irep_idt &identifier=
function.get(ID_identifier);
298 if(recursion_set.find(identifier)!=recursion_set.end())
304 recursion_set.insert(identifier);
306 goto_functionst::function_mapt::const_iterator it=
310 throw "failed to find function "+
id2string(identifier);
320 recursion_set.erase(identifier);
322 else if(
function.
id()==ID_if)
324 if(
function.operands().size()!=3)
325 throw "if takes three arguments";
328 do_function_call_rec(
336 do_function_call_rec(
341 goto_functions) || new_data;
343 else if(
function.
id()==ID_dereference)
351 for(
const auto &v : values)
353 if(v.id()==ID_object_descriptor)
358 goto_functionst::function_mapt::const_iterator it=
364 do_function_call_rec(
369 goto_functions) || new_data;
374 else if(
function.
id()==
"NULL-object")
378 else if(
function.
id()==ID_member ||
function.id()==ID_index)
382 else if(
function.
id()==
"builtin-function")
388 throw "unexpected function_call argument: "+
389 function.id_string();
400 if(functions_done.find(it->first)==
401 functions_done.end())
403 fixedpoint(it, goto_functions);
408 const goto_functionst::function_mapt::const_iterator it,
411 functions_done.insert(it->first);
412 return fixedpoint(it->second.body, goto_functions);
const irept & get_nil_irep()
bool body_available() const
targett add_instruction()
Adds an instruction at the end.
exprt get_guard(locationt from, locationt to) const
const std::string & id2string(const irep_idt &d)
instructionst instructions
The list of instructions in the goto program.
virtual void operator()(const goto_programt &goto_program)
locationt get_next(working_sett &working_set)
virtual bool transform(const namespacet &ns, locationt from, locationt to)=0
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 void output(const namespacet &ns, std::ostream &out) const
std::list< Target > get_successors(Target target) const
goto_programt::const_targett locationt
The boolean constant true.
flow_insensitive_abstract_domain_baset::expr_sett expr_sett
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)
API to expression classes.
const irep_idt & get(const irep_namet &name) const
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
function_mapt function_map
std::vector< exprt > operandst
const object_descriptor_exprt & to_object_descriptor_expr(const exprt &expr)
Cast a generic exprt to an object_descriptor_exprt.
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
Flow Insensitive Static Analysis.
exprt get_return_lhs(locationt to) const
Base class for all expressions.
virtual void initialize(const namespacet &ns)=0
const codet & to_code(const exprt &expr)
#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)
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)
instructionst::iterator targett
virtual void get_reference_set(const namespacet &ns, const exprt &expr, expr_sett &expr_set)