Go to the documentation of this file.
31 bool _base_case,
bool _step_case,
60 assert(!loop.empty());
63 const exprt loop_guard=loop_head->guard;
78 assume.
guard=loop_guard;
95 std::vector<goto_programt::targett> iteration_points;
115 assert(iteration_points.size()==
k+1);
129 assume.
guard=loop_guard;
145 for(natural_loops_mutablet::loop_mapt::const_iterator
154 bool base_case,
bool step_case,
k_inductiont(goto_functiont &_goto_function, bool _base_case, bool _step_case, unsigned _k)
goto_functiont & goto_function
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
Base class for all expressions.
natural_loops_mutablet natural_loops
void process_loop(const goto_programt::targett loop_head, const loopt &)
goto_functionst::goto_functiont goto_functiont
std::set< exprt > modifiest
goto_programt::targett get_loop_exit(const loopt &loop)
void unwind(goto_programt &goto_program, const goto_programt::const_targett loop_head, const goto_programt::const_targett loop_exit, const unsigned k, const unwind_strategyt unwind_strategy)
void k_induction(goto_modelt &goto_model, bool base_case, bool step_case, unsigned k)
A goto function, consisting of function type (see type), function body (see body),...
#define Forall_goto_functions(it, functions)
::goto_functiont goto_functiont
instructionst instructions
The list of instructions in the goto program.
local_may_aliast local_may_alias
goto_functionst goto_functions
GOTO functions.
void get_modifies(const local_may_aliast &local_may_alias, const loopt &loop, modifiest &modifies)
exprt guard
Guard for gotos, assume, assert.
A generic container class for the GOTO intermediate representation of one function.
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
const typedef natural_loops_mutablet::natural_loopt loopt
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.
instructionst::iterator targett