22 assert(!loop.empty());
25 std::map<unsigned, goto_programt::targett> loop_map;
30 loop_map[(*l_it)->location_number]=*l_it;
43 for(modifiest::const_iterator
44 m_it=modifies.begin();
54 t->code.add_source_location()=loop_head->source_location;
64 if(lhs.
id()==ID_symbol)
66 else if(lhs.
id()==ID_dereference)
69 for(modifiest::const_iterator m_it=m.begin();
70 m_it!=m.end(); m_it++)
73 else if(lhs.
id()==ID_member)
76 else if(lhs.
id()==ID_index)
79 else if(lhs.
id()==ID_if)
94 i_it=loop.begin(); i_it!=loop.end(); i_it++)
A codet representing an assignment in the program.
Base class for all expressions.
const source_locationt & source_location() const
typet & type()
Return the type of the expression.
This class represents an instruction in the GOTO intermediate representation.
codet code
Do not read or modify directly – use get_X() instead.
bool is_function_call() const
A generic container class for the GOTO intermediate representation of one function.
instructionst::iterator targett
instructionst::const_iterator const_targett
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
targett add(instructiont &&instruction)
Adds a given instruction at the end.
The trinary if-then-else operator.
const irep_idt & id() const
std::set< exprt > get(const goto_programt::const_targett t, const exprt &src) const
loop_instructionst::const_iterator const_iterator
A side_effect_exprt that returns a non-deterministically chosen value.
const source_locationt & source_location() const
Field-insensitive, location-sensitive may-alias analysis.
void get_modifies(const local_may_aliast &local_may_alias, const loopt &loop, modifiest &modifies)
goto_programt::targett get_loop_exit(const loopt &loop)
void build_havoc_code(const goto_programt::targett loop_head, const modifiest &modifies, goto_programt &dest)
void get_modifies_lhs(const local_may_aliast &local_may_alias, goto_programt::const_targett t, const exprt &lhs, modifiest &modifies)
Helper functions for k-induction and loop invariants.
natural_loops_mutablet::natural_loopt loopt
std::set< exprt > modifiest
Compute natural loops in a goto_function.
API to expression classes for Pointers.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
const code_function_callt & to_code_function_call(const codet &code)
const code_assignt & to_code_assign(const codet &code)
API to expression classes.
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.