Go to the documentation of this file.
12 #ifndef CPROVER_GOTO_INSTRUMENT_LOOP_UTILS_H
13 #define CPROVER_GOTO_INSTRUMENT_LOOP_UTILS_H
40 #endif // CPROVER_GOTO_INSTRUMENT_LOOP_UTILS_H
Base class for all expressions.
natural_loops_mutablet::natural_loopt loopt
void get_modifies_lhs(const local_may_aliast &local_may_alias, goto_programt::const_targett t, const exprt &lhs, modifiest &modifies)
std::set< exprt > modifiest
A loop, specified as a set of instructions.
Compute natural loops in a goto_function.
void get_modifies(const local_may_aliast &local_may_alias, const loopt &loop, modifiest &modifies)
void build_havoc_code(const goto_programt::targett loop_head, const modifiest &modifies, goto_programt &dest)
A generic container class for the GOTO intermediate representation of one function.
instructionst::const_iterator const_targett
instructionst::iterator targett
goto_programt::targett get_loop_exit(const loopt &)