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 local_may_aliast &local_may_alias, const goto_programt::const_targett, modifiest &)
function_mapt function_map
::goto_functiont goto_functiont
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
goto_functionst goto_functions
GOTO functions.
This class represents an instruction in the GOTO intermediate representation.
targetst targets
The list of successor instructions.
A generic container class for the GOTO intermediate representation of one function.
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
instructionst::iterator targett
void get_modifies(const loopt &, modifiest &)
const natural_loops_mutablet::natural_loopt loopt
void havoc_loop(const goto_programt::targett loop_head, const loopt &)
goto_functiont & goto_function
havoc_loopst(function_modifiest &_function_modifies, goto_functiont &_goto_function)
local_may_aliast local_may_alias
function_modifiest & function_modifies
goto_functionst::goto_functiont goto_functiont
natural_loops_mutablet natural_loops
std::set< exprt > modifiest
loop_instructionst::const_iterator const_iterator
parentt::loopt natural_loopt
void havoc_loops(goto_modelt &goto_model)
Field-insensitive, location-sensitive may-alias analysis.
goto_programt::targett get_loop_exit(const loopt &loop)
void build_havoc_code(const goto_programt::targett loop_head, const modifiest &modifies, goto_programt &dest)
Helper functions for k-induction and loop invariants.
Compute natural loops in a goto_function.
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
API to expression classes.