Go to the documentation of this file.
45 assert(!loop.empty());
48 std::map<unsigned, goto_programt::targett> loop_map;
53 loop_map[(*l_it)->location_number]=*l_it;
70 t->code_nonconst().add_source_location() = loop_head->source_location;
78 codet havoc(ID_havoc_object);
91 for(
const auto &lhs : modifies)
93 if(lhs.id() == ID_index || lhs.id() == ID_dereference)
113 if(lhs.
id() == ID_symbol || lhs.
id() == ID_member || lhs.
id() == ID_index)
114 modifies.insert(lhs);
115 else if(lhs.
id()==ID_dereference)
118 for(
const auto &mod : local_may_alias.
get(t, ptr.
pointer))
126 else if(lhs.
id()==ID_if)
141 i_it=loop.begin(); i_it!=loop.end(); i_it++)
Determine whether an expression is constant.
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.
void build_havoc_code_for_object(const goto_programt::targett loop_head, const exprt &lhs, goto_programt &dest)
targett add(instructiont &&instruction)
Adds a given instruction at the end.
The plus expression Associativity is not specified.
Base class for all expressions.
bool is_constant(const exprt &expr) const override
This function determines what expressions are to be propagated as "constants".
natural_loops_mutablet::natural_loopt loopt
const code_assignt & get_assign() const
Get the assignment for ASSIGN.
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
virtual bool is_constant(const exprt &) const
This function determines what expressions are to be propagated as "constants".
typet & type()
Return the type of the expression.
std::set< exprt > modifiest
loop_instructionst::const_iterator const_iterator
Field-insensitive, location-sensitive may-alias analysis.
goto_programt::targett get_loop_exit(const loopt &loop)
const source_locationt & source_location() const
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.
const code_function_callt & get_function_call() const
Get the function call for FUNCTION_CALL.
void build_havoc_code_for_scalar(const goto_programt::targett loop_head, const exprt &lhs, goto_programt &dest)
const irep_idt & id() const
Helper functions for k-induction and loop invariants.
A side_effect_exprt that returns a non-deterministically chosen value.
loop_utils_is_constantt(const modifiest &mod)
Deprecated expression utility functions.
void get_modifies(const local_may_aliast &local_may_alias, const loopt &loop, modifiest &modifies)
Compute natural loops in a goto_function.
static instructiont make_other(const codet &_code, const source_locationt &l=source_locationt::nil())
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
A generic container class for the GOTO intermediate representation of one function.
instructionst::const_iterator const_targett
Operator to return the address of an object.
source_locationt & add_source_location()
void build_havoc_code(const goto_programt::targett loop_head, const modifiest &modifies, goto_programt &dest)
bool is_function_call() const
std::set< exprt > get(const goto_programt::const_targett t, const exprt &src) const
bool is_constant(const typet &type)
This method tests, if the given typet is a constant.
This class represents an instruction in the GOTO intermediate representation.
API to expression classes.
const source_locationt & source_location() const
instructionst::iterator targett
Data structure for representing an arbitrary statement in a program.
const modifiest & modifies