Go to the documentation of this file.
64 assert(!loop.empty());
67 const exprt loop_guard=loop_head->guard;
104 std::vector<goto_programt::targett> iteration_points;
125 assert(iteration_points.size()==
k+1);
155 for(natural_loops_mutablet::loop_mapt::const_iterator
164 bool base_case,
bool step_case,
168 k_inductiont(it->first, it->second, base_case, step_case, k);
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
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 unwind(const irep_idt &function_id, 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 process_loop(const goto_programt::targett loop_head, const loopt &)
natural_loops_mutablet::natural_loopt loopt
std::set< exprt > modifiest
Field-insensitive, location-sensitive may-alias analysis.
goto_programt::targett get_loop_exit(const loopt &loop)
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)
Helper functions for k-induction and loop invariants.
instructionst instructions
The list of instructions in the goto program.
local_may_aliast local_may_alias
goto_functionst goto_functions
GOTO functions.
const irep_idt & function_id
void get_modifies(const local_may_aliast &local_may_alias, const loopt &loop, modifiest &modifies)
Compute natural loops in a goto_function.
A generic container class for the GOTO intermediate representation of one function.
static instructiont make_assumption(const exprt &g, const source_locationt &l=source_locationt::nil())
k_inductiont(const irep_idt &_function_id, goto_functiont &_goto_function, bool _base_case, bool _step_case, unsigned _k)
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
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.
API to expression classes.
instructionst::iterator targett