cprover
|
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< exprt > | modifiest |
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 | |
const typedef natural_loops_mutablet::natural_loopt | loopt |
goto_functiont & | goto_function |
local_may_aliast | local_may_alias |
function_modifiest & | function_modifies |
natural_loops_mutablet | natural_loops |
Definition at line 23 of file havoc_loops.cpp.
Definition at line 26 of file havoc_loops.cpp.
|
protected |
Definition at line 45 of file havoc_loops.cpp.
|
inline |
Definition at line 28 of file havoc_loops.cpp.
|
protected |
Definition at line 84 of file havoc_loops.cpp.
|
protected |
Definition at line 66 of file havoc_loops.cpp.
Definition at line 150 of file havoc_loops.cpp.
|
protected |
Definition at line 106 of file havoc_loops.cpp.
|
protected |
Definition at line 180 of file havoc_loops.cpp.
|
protected |
Definition at line 42 of file havoc_loops.cpp.
|
protected |
Definition at line 40 of file havoc_loops.cpp.
|
protected |
Definition at line 41 of file havoc_loops.cpp.
|
protected |
Definition at line 46 of file havoc_loops.cpp.
|
protected |
Definition at line 43 of file havoc_loops.cpp.