Go to the documentation of this file.
64 assert(!loop.empty());
84 l_it=loop.begin(); l_it!=loop.end(); l_it++)
89 for(goto_programt::targetst::iterator
90 t_it=instruction.
targets.begin();
91 t_it!=instruction.
targets.end();
108 for(
const auto &instruction_it : loop)
void get_modifies(const loopt &, modifiest &)
goto_functionst::goto_functiont goto_functiont
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
targetst targets
The list of successor instructions.
havoc_loopst(function_modifiest &_function_modifies, goto_functiont &_goto_function)
goto_functiont & goto_function
loop_instructionst::const_iterator const_iterator
const natural_loops_mutablet::natural_loopt loopt
Field-insensitive, location-sensitive may-alias analysis.
goto_programt::targett get_loop_exit(const loopt &loop)
std::set< exprt > modifiest
A goto function, consisting of function type (see type), function body (see body),...
natural_loops_mutablet natural_loops
local_may_aliast local_may_alias
#define Forall_goto_functions(it, functions)
Helper functions for k-induction and loop invariants.
parentt::loopt natural_loopt
::goto_functiont goto_functiont
goto_functionst goto_functions
GOTO functions.
void get_modifies(const local_may_aliast &local_may_alias, const goto_programt::const_targett, modifiest &)
Compute natural loops in a goto_function.
void havoc_loop(const goto_programt::targett loop_head, const loopt &)
A generic container class for the GOTO intermediate representation of one function.
function_modifiest & function_modifies
void havoc_loops(goto_modelt &goto_model)
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
void build_havoc_code(const goto_programt::targett loop_head, const modifiest &modifies, goto_programt &dest)
This class represents an instruction in the GOTO intermediate representation.
API to expression classes.
instructionst::iterator targett