Go to the documentation of this file.
63 assert(!loop.empty());
83 l_it=loop.begin(); l_it!=loop.end(); l_it++)
88 for(goto_programt::targetst::iterator
89 t_it=instruction.
targets.begin();
90 t_it!=instruction.
targets.end();
107 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
Utilities for building havoc code for expressions.
targetst targets
The list of successor instructions.
function_mapt function_map
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 body (see body) and parameter identifiers (see parameter_iden...
natural_loops_mutablet natural_loops
local_may_aliast local_may_alias
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 append_havoc_code(const source_locationt source_location, const modifiest &modifies, goto_programt &dest)
void havoc_loops(goto_modelt &goto_model)
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
This class represents an instruction in the GOTO intermediate representation.
instructionst::iterator targett