30 goto_functiont &_goto_function,
31 bool _base_case,
bool _step_case,
60 assert(!loop.empty());
63 const exprt loop_guard=loop_head->guard;
77 goto_programt::instructiont assume(
ASSUME);
78 assume.guard=loop_guard;
95 std::vector<goto_programt::targett> iteration_points;
115 assert(iteration_points.size()==
k+1);
128 goto_programt::instructiont assume(
ASSUME);
129 assume.guard=loop_guard;
145 for(natural_loops_mutablet::loop_mapt::const_iterator
goto_functionst::goto_functiont goto_functiont
local_may_aliast local_may_alias
void process_loop(const goto_programt::targett loop_head, const loopt &)
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
API to expression classes.
goto_programt::targett get_loop_exit(const loopt &loop)
std::set< exprt > modifiest
Helper functions for k-induction and loop invariants.
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
void remove_skip(goto_programt &goto_program)
remove unnecessary skip statements
void get_modifies(const local_may_aliast &local_may_alias, const loopt &loop, modifiest &modifies)
Base class for all expressions.
#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)
Field-insensitive, location-sensitive may-alias analysis.
instructionst::iterator targett