cprover
Public Types | Public Member Functions | Protected Member Functions | Protected Attributes | List of all members
k_inductiont Class Reference
+ Collaboration diagram for k_inductiont:

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
 

Detailed Description

Definition at line 24 of file k_induction.cpp.

Member Typedef Documentation

◆ goto_functiont

typedef goto_functionst::goto_functiont k_inductiont::goto_functiont

Definition at line 27 of file k_induction.cpp.

Constructor & Destructor Documentation

◆ k_inductiont()

k_inductiont::k_inductiont ( goto_functiont &  _goto_function,
bool  _base_case,
bool  _step_case,
unsigned  _k 
)
inline

Definition at line 29 of file k_induction.cpp.

Member Function Documentation

◆ k_induction()

void k_inductiont::k_induction ( )
protected

Definition at line 141 of file k_induction.cpp.

◆ process_loop()

void k_inductiont::process_loop ( const goto_programt::targett  loop_head,
const loopt &  loop 
)
protected

Definition at line 56 of file k_induction.cpp.

Member Data Documentation

◆ base_case

const bool k_inductiont::base_case
protected

Definition at line 46 of file k_induction.cpp.

◆ goto_function

goto_functiont& k_inductiont::goto_function
protected

Definition at line 42 of file k_induction.cpp.

◆ k

const unsigned k_inductiont::k
protected

Definition at line 47 of file k_induction.cpp.

◆ local_may_alias

local_may_aliast k_inductiont::local_may_alias
protected

Definition at line 43 of file k_induction.cpp.

◆ natural_loops

natural_loops_mutablet k_inductiont::natural_loops
protected

Definition at line 44 of file k_induction.cpp.

◆ step_case

const bool k_inductiont::step_case
protected

Definition at line 46 of file k_induction.cpp.

The documentation for this class was generated from the following file: