cprover
havoc_loopst Class Reference
Collaboration diagram for havoc_loopst:
[legend]

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 build_havoc_code (const goto_programt::targett loop_head, const modifiest &modifies, goto_programt &dest)
 
void get_modifies (const loopt &, modifiest &)
 
goto_programt::targett get_loop_exit (const loopt &)
 

Protected Attributes

goto_functiontgoto_function
 
local_may_aliast local_may_alias
 
function_modifiestfunction_modifies
 
natural_loops_mutablet natural_loops
 

Detailed Description

Definition at line 23 of file havoc_loops.cpp.

Member Typedef Documentation

§ goto_functiont

§ loopt

Definition at line 46 of file havoc_loops.cpp.

§ modifiest

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

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

References havoc_loops().

Referenced by havoc_loops().

Member Function Documentation

§ build_havoc_code()

void havoc_loopst::build_havoc_code ( const goto_programt::targett  loop_head,
const modifiest modifies,
goto_programt dest 
)
protected

§ get_loop_exit()

goto_programt::targett havoc_loopst::get_loop_exit ( const loopt loop)
protected

Definition at line 66 of file havoc_loops.cpp.

Referenced by havoc_loop().

§ get_modifies()

§ havoc_loop()

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

§ havoc_loops()

void havoc_loopst::havoc_loops ( )
protected

Definition at line 179 of file havoc_loops.cpp.

References havoc_loop(), natural_loops_templatet< P, T >::loop_map, and natural_loops.

Referenced by havoc_loopst().

Member Data Documentation

§ function_modifies

function_modifiest& havoc_loopst::function_modifies
protected

Definition at line 42 of file havoc_loops.cpp.

Referenced by get_modifies(), and havoc_loops().

§ goto_function

goto_functiont& havoc_loopst::goto_function
protected

Definition at line 40 of file havoc_loops.cpp.

Referenced by havoc_loop().

§ local_may_alias

local_may_aliast havoc_loopst::local_may_alias
protected

Definition at line 41 of file havoc_loops.cpp.

Referenced by get_modifies().

§ natural_loops

natural_loops_mutablet havoc_loopst::natural_loops
protected

Definition at line 43 of file havoc_loops.cpp.

Referenced by havoc_loops().


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