25 else if(std::next(from) == to)
28 return from->get_condition();
36 if(to->is_end_function())
40 return to->call_lhs();
55 fixedpoint(function_id, goto_program, goto_functions);
65 <<
"//// Function: " <<
gf_entry.first <<
"\n////\n\n";
135 std::cout <<
"Visiting: " << l->function <<
" " <<
136 l->location_number <<
'\n';
152 if(l->is_function_call())
164 changed =
get_state().transform(
ns, function_id, l, function_id,
to_l);
194 const goto_functionst::function_mapt::const_iterator
f_it,
200 if(!goto_function.body_available())
206 l_call->call_lhs().type(),
l_call->source_location())));
207 r->location_number=0;
210 t->location_number=1;
226 assert(!goto_function.body.instructions.empty());
275 const exprt &function,
294 goto_functionst::function_mapt::const_iterator it=
298 throw "failed to find function "+
id2string(identifier);
301 calling_function,
l_call, goto_functions, it, arguments, state);
334 for(
const auto &v : values)
341 goto_functionst::function_mapt::const_iterator it=
366 else if(function.
id()==
"builtin-function")
372 throw "unexpected function_call argument: "+
virtual void output(const namespacet &ns, const irep_idt &function_id, const goto_programt &goto_program, std::ostream &out) const
Output the abstract states for a single function.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
std::vector< exprt > operandst
exprt get_guard(locationt from, locationt to) const
exprt get_return_lhs(locationt to) const
virtual bool transform(const namespacet &ns, const irep_idt &function_from, locationt from, const irep_idt &function_to, locationt to)=0
goto_programt::const_targett locationt
functions_donet functions_done
std::set< locationt > seen_locations
virtual void output(const goto_functionst &goto_functions, std::ostream &out)
virtual void operator()(const irep_idt &function_id, const goto_programt &goto_program)
virtual void get_reference_set(const exprt &expr, expr_sett &expr_set)=0
locationt get_next(working_sett &working_set)
recursion_sett recursion_set
bool fixedpoint(const irep_idt &function_id, const goto_programt &goto_program, const goto_functionst &goto_functions)
bool seen(const locationt &l)
bool visit(const irep_idt &function_id, locationt l, working_sett &working_set, const goto_programt &goto_program, const goto_functionst &goto_functions)
virtual void update(const goto_programt &goto_program)
flow_insensitive_abstract_domain_baset::expr_sett expr_sett
bool do_function_call_rec(const irep_idt &calling_function, locationt l_call, const exprt &function, const exprt::operandst &arguments, statet &new_state, const goto_functionst &goto_functions)
goto_programt::const_targett locationt
virtual void initialize(const goto_programt &)
std::priority_queue< locationt > working_sett
std::map< locationt, unsigned > statistics
void put_in_working_set(working_sett &working_set, locationt l)
bool do_function_call(const irep_idt &calling_function, locationt l_call, const goto_functionst &goto_functions, const goto_functionst::function_mapt::const_iterator f_it, const exprt::operandst &arguments, statet &new_state)
virtual statet & get_state()=0
A collection of goto functions.
function_mapt function_map
::goto_functiont goto_functiont
A generic container class for the GOTO intermediate representation of one function.
instructionst instructions
The list of instructions in the goto program.
static instructiont make_set_return_value(exprt return_value, const source_locationt &l=source_locationt::nil())
static instructiont make_end_function(const source_locationt &l=source_locationt::nil())
instructionst::iterator targett
std::list< Target > get_successors(Target target) const
Get control-flow successors of a given instruction.
const irep_idt & get(const irep_idt &name) const
const std::string & id_string() const
const irep_idt & id() const
Split an expression into a base object and a (byte) offset.
A side_effect_exprt that returns a non-deterministically chosen value.
const irep_idt & get_identifier() const
The Boolean constant true.
exprt boolean_negate(const exprt &src)
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true
Deprecated expression utility functions.
Flow Insensitive Static Analysis.
const irept & get_nil_irep()
const std::string & id2string(const irep_idt &d)
API to expression classes for Pointers.
const object_descriptor_exprt & to_object_descriptor_expr(const exprt &expr)
Cast an exprt to an object_descriptor_exprt.
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.