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

Public Types

typedef goto_functionst::goto_functiont goto_functiont
 

Public Member Functions

 havoc_loopst (function_assignst &_function_assigns, goto_functiont &_goto_function, const namespacet &ns)
 

Protected Types

typedef std::set< exprt > assignst
 
typedef const natural_loops_mutablet::natural_loopt loopt
 

Protected Member Functions

void havoc_loops ()
 
void havoc_loop (const goto_programt::targett loop_head, const loopt &)
 
void get_assigns (const loopt &, assignst &)
 

Protected Attributes

goto_functiont & goto_function
 
local_may_aliast local_may_alias
 
function_assignst & function_assigns
 
natural_loops_mutablet natural_loops
 
const namespacet & ns
 

Detailed Description

Definition at line 23 of file havoc_loops.cpp.

Member Typedef Documentation

◆ assignst

typedef std::set<exprt> havoc_loopst::assignst
protected

Definition at line 48 of file havoc_loops.cpp.

◆ goto_functiont

typedef goto_functionst::goto_functiont havoc_loopst::goto_functiont

Definition at line 26 of file havoc_loops.cpp.

◆ loopt

typedef const natural_loops_mutablet::natural_loopt havoc_loopst::loopt
protected

Definition at line 49 of file havoc_loops.cpp.

Constructor & Destructor Documentation

◆ havoc_loopst()

havoc_loopst::havoc_loopst ( function_assignst &  _function_assigns,
goto_functiont &  _goto_function,
const namespacet &  ns 
)
inline

Definition at line 28 of file havoc_loops.cpp.

Member Function Documentation

◆ get_assigns()

void havoc_loopst::get_assigns ( const loopt &  loop,
assignst &  assigns 
)
protected

Definition at line 105 of file havoc_loops.cpp.

◆ havoc_loop()

void havoc_loopst::havoc_loop ( const goto_programt::targett  loop_head,
const loopt &  loop 
)
protected

Definition at line 60 of file havoc_loops.cpp.

◆ havoc_loops()

void havoc_loopst::havoc_loops ( )
protected

Definition at line 111 of file havoc_loops.cpp.

Member Data Documentation

◆ function_assigns

function_assignst& havoc_loopst::function_assigns
protected

Definition at line 44 of file havoc_loops.cpp.

◆ goto_function

goto_functiont& havoc_loopst::goto_function
protected

Definition at line 42 of file havoc_loops.cpp.

◆ local_may_alias

local_may_aliast havoc_loopst::local_may_alias
protected

Definition at line 43 of file havoc_loops.cpp.

◆ natural_loops

natural_loops_mutablet havoc_loopst::natural_loops
protected

Definition at line 45 of file havoc_loops.cpp.

◆ ns

const namespacet& havoc_loopst::ns
protected

Definition at line 46 of file havoc_loops.cpp.

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