Go to the documentation of this file.
23 assert(!loop.
empty());
26 std::map<unsigned, goto_programt::targett> loop_map;
31 loop_map[(*l_it)->location_number]=*l_it;
46 if(lhs.
id() == ID_symbol || lhs.
id() == ID_member || lhs.
id() == ID_index)
48 else if(lhs.
id()==ID_dereference)
51 for(
const auto &mod : local_may_alias.
get(t, ptr.
pointer))
59 else if(lhs.
id()==ID_if)
74 i_it=loop.
begin(); i_it!=loop.
end(); i_it++)
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Operator to dereference a pointer.
The trinary if-then-else operator.
The plus expression Associativity is not specified.
const_iterator end() const
Iterator over this loop's instructions.
Base class for all expressions.
const code_assignt & get_assign() const
Get the assignment for ASSIGN.
std::set< exprt > modifiest
const_iterator begin() const
Iterator over this loop's instructions.
loop_instructionst::const_iterator const_iterator
Field-insensitive, location-sensitive may-alias analysis.
goto_programt::targett get_loop_exit(const loopt &loop)
void get_modifies_lhs(const local_may_aliast &local_may_alias, goto_programt::const_targett t, const exprt &lhs, modifiest &modifies)
API to expression classes for Pointers.
A loop, specified as a set of instructions.
const irep_idt & id() const
const exprt & call_lhs() const
Get the lhs of a FUNCTION_CALL (may be nil)
Helper functions for k-induction and loop invariants.
void get_modifies(const local_may_aliast &local_may_alias, const loopt &loop, modifiest &modifies)
bool empty() const
Returns true if this loop contains no instructions.
instructionst::const_iterator const_targett
bool is_function_call() const
std::set< exprt > get(const goto_programt::const_targett t, const exprt &src) const
This class represents an instruction in the GOTO intermediate representation.
API to expression classes.
instructionst::iterator targett