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.
References k_induction().
|
protected |
Definition at line 141 of file k_induction.cpp.
References natural_loops_templatet< P, T >::loop_map, natural_loops, and process_loop().
Referenced by k_inductiont().
|
protected |
Definition at line 56 of file k_induction.cpp.
References ASSUME, base_case, goto_function_templatet< bodyT >::body, build_havoc_code(), get_loop_exit(), get_modifies(), goto_function, k, local_may_alias, goto_unwindt::PARTIAL, remove_skip(), step_case, and goto_unwindt::unwind().
Referenced by k_induction().
|
protected |
Definition at line 46 of file k_induction.cpp.
Referenced by process_loop().
|
protected |
Definition at line 42 of file k_induction.cpp.
Referenced by process_loop().
|
protected |
Definition at line 47 of file k_induction.cpp.
Referenced by process_loop().
|
protected |
Definition at line 43 of file k_induction.cpp.
Referenced by process_loop().
|
protected |
Definition at line 44 of file k_induction.cpp.
Referenced by k_induction().
|
protected |
Definition at line 46 of file k_induction.cpp.
Referenced by process_loop().