cprover
|
Public Types | |
typedef goto_functionst::goto_functiont | goto_functiont |
Public Member Functions | |
k_inductiont (goto_functiont &_goto_function, bool _base_case, bool _step_case, unsigned _k) | |
Protected Member Functions | |
void | k_induction () |
void | process_loop (const goto_programt::targett loop_head, const loopt &) |
Protected Attributes | |
goto_functiont & | goto_function |
local_may_aliast | local_may_alias |
natural_loops_mutablet | natural_loops |
const bool | base_case |
const bool | step_case |
const unsigned | k |
Definition at line 24 of file k_induction.cpp.
Definition at line 27 of file k_induction.cpp.
|
inline |
Definition at line 29 of file k_induction.cpp.
|
protected |
Definition at line 141 of file k_induction.cpp.
|
protected |
Definition at line 56 of file k_induction.cpp.
|
protected |
Definition at line 46 of file k_induction.cpp.
|
protected |
Definition at line 42 of file k_induction.cpp.
|
protected |
Definition at line 47 of file k_induction.cpp.
|
protected |
Definition at line 43 of file k_induction.cpp.
|
protected |
Definition at line 44 of file k_induction.cpp.
|
protected |
Definition at line 46 of file k_induction.cpp.