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

Public Member Functions

 k_inductiont (const irep_idt &_function_id, goto_functiont &_goto_function, bool _base_case, bool _step_case, unsigned _k, const namespacet &ns)
 

Protected Member Functions

void k_induction ()
 
void process_loop (const goto_programt::targett loop_head, const loopt &)
 

Protected Attributes

const irep_idt & function_id
 
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
 
const namespacet & ns
 

Detailed Description

Definition at line 23 of file k_induction.cpp.

Constructor & Destructor Documentation

◆ k_inductiont()

k_inductiont::k_inductiont ( const irep_idt &  _function_id,
goto_functiont &  _goto_function,
bool  _base_case,
bool  _step_case,
unsigned  _k,
const namespacet &  ns 
)
inline

Definition at line 26 of file k_induction.cpp.

Member Function Documentation

◆ k_induction()

void k_inductiont::k_induction ( )
protected

Definition at line 157 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 63 of file k_induction.cpp.

Member Data Documentation

◆ base_case

const bool k_inductiont::base_case
protected

Definition at line 51 of file k_induction.cpp.

◆ function_id

const irep_idt& k_inductiont::function_id
protected

Definition at line 46 of file k_induction.cpp.

◆ goto_function

goto_functiont& k_inductiont::goto_function
protected

Definition at line 47 of file k_induction.cpp.

◆ k

const unsigned k_inductiont::k
protected

Definition at line 52 of file k_induction.cpp.

◆ local_may_alias

local_may_aliast k_inductiont::local_may_alias
protected

Definition at line 48 of file k_induction.cpp.

◆ natural_loops

natural_loops_mutablet k_inductiont::natural_loops
protected

Definition at line 49 of file k_induction.cpp.

◆ ns

const namespacet& k_inductiont::ns
protected

Definition at line 54 of file k_induction.cpp.

◆ step_case

const bool k_inductiont::step_case
protected

Definition at line 51 of file k_induction.cpp.

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