12 #ifndef CPROVER_GOTO_INSTRUMENT_LOOP_UTILS_H 13 #define CPROVER_GOTO_INSTRUMENT_LOOP_UTILS_H 34 #endif // CPROVER_GOTO_INSTRUMENT_LOOP_UTILS_H void get_modifies(const local_may_aliast &local_may_alias, const loopt &loop, modifiest &modifies)
std::set< goto_programt::targett > natural_loopt
const natural_loops_mutablet::natural_loopt loopt
std::set< exprt > modifiest
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
goto_programt::targett get_loop_exit(const loopt &)
void build_havoc_code(const goto_programt::targett loop_head, const modifiest &modifies, goto_programt &dest)
Compute natural loops in a goto_function.
instructionst::iterator targett