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,
exprt guard
Guard for gotos, assume, assert.
goto_functionst::goto_functiont goto_functiont
local_may_aliast local_may_alias
void process_loop(const goto_programt::targett loop_head, const loopt &)
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
const natural_loops_mutablet::natural_loopt loopt
goto_functiont & goto_function
k_inductiont(goto_functiont &_goto_function, bool _base_case, bool _step_case, unsigned _k)
natural_loops_mutablet natural_loops
This class represents an instruction in the GOTO intermediate representation.
instructionst::iterator targett
instructionst instructions
The list of instructions in the goto program.
API to expression classes.
goto_programt::targett get_loop_exit(const loopt &loop)
::goto_functiont goto_functiont
std::set< exprt > modifiest
Helper functions for k-induction and loop invariants.
A goto function, consisting of function type (see type), function body (see body),...
A generic container class for the GOTO intermediate representation of one function.
void get_modifies(const local_may_aliast &local_may_alias, const loopt &loop, modifiest &modifies)
void k_induction(goto_modelt &goto_model, bool base_case, bool step_case, unsigned k)
Base class for all expressions.
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
#define Forall_goto_functions(it, functions)
void build_havoc_code(const goto_programt::targett loop_head, const modifiest &modifies, goto_programt &dest)
Compute natural loops in a goto_function.
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)
goto_functionst goto_functions
GOTO functions.
Field-insensitive, location-sensitive may-alias analysis.