cprover
havoc_loopst Class Reference
+ Collaboration diagram for havoc_loopst:

Public Types

typedef goto_functionst::goto_functiont goto_functiont
 

Public Member Functions

 havoc_loopst (function_modifiest &_function_modifies, goto_functiont &_goto_function)
 

Protected Types

typedef std::set< exprtmodifiest
 
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_modifies (const loopt &, modifiest &)
 

Protected Attributes

goto_functiontgoto_function
 
local_may_aliast local_may_alias
 
function_modifiestfunction_modifies
 
natural_loops_mutablet natural_loops
 

Detailed Description

Definition at line 24 of file havoc_loops.cpp.

Member Typedef Documentation

◆ goto_functiont

◆ loopt

Definition at line 47 of file havoc_loops.cpp.

◆ modifiest

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

Definition at line 46 of file havoc_loops.cpp.

Constructor & Destructor Documentation

◆ havoc_loopst()

havoc_loopst::havoc_loopst ( function_modifiest _function_modifies,
goto_functiont _goto_function 
)
inline

Definition at line 29 of file havoc_loops.cpp.

Member Function Documentation

◆ get_modifies()

void havoc_loopst::get_modifies ( const loopt loop,
modifiest modifies 
)
protected

Definition at line 104 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 112 of file havoc_loops.cpp.

Member Data Documentation

◆ function_modifies

function_modifiest& havoc_loopst::function_modifies
protected

Definition at line 43 of file havoc_loops.cpp.

◆ goto_function

goto_functiont& havoc_loopst::goto_function
protected

Definition at line 41 of file havoc_loops.cpp.

◆ local_may_alias

local_may_aliast havoc_loopst::local_may_alias
protected

Definition at line 42 of file havoc_loops.cpp.

◆ natural_loops

natural_loops_mutablet havoc_loopst::natural_loops
protected

Definition at line 44 of file havoc_loops.cpp.


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