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().

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

Definition at line 84 of file havoc_loops.cpp.

References goto_programt::add_instruction(), ASSIGN, typet::source_location(), and exprt::type().

Referenced by havoc_loop().

◆ 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()

◆ havoc_loops()

void havoc_loopst::havoc_loops ( )
protected

Definition at line 180 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().

◆ 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: