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 |
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_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 46 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.
References havoc_loops().
|
protected |
Definition at line 84 of file havoc_loops.cpp.
References goto_programt::add_instruction(), ASSIGN, and exprt::type().
Referenced by havoc_loop().
|
protected |
Definition at line 66 of file havoc_loops.cpp.
Referenced by havoc_loop().
Definition at line 149 of file havoc_loops.cpp.
References goto_programt::instructiont::code, code_function_callt::function(), function_modifies, function_modifiest::get_modifies_lhs(), goto_programt::instructiont::is_assign(), goto_programt::instructiont::is_function_call(), irept::is_not_nil(), code_assignt::lhs(), code_function_callt::lhs(), local_may_alias, to_code_assign(), and to_code_function_call().
Referenced by havoc_loop().
|
protected |
Definition at line 105 of file havoc_loops.cpp.
References goto_functiont::body, build_havoc_code(), get_loop_exit(), get_modifies(), goto_function, goto_programt::insert_before_swap(), goto_programt::instructiont::is_goto(), remove_skip(), and goto_programt::instructiont::targets.
Referenced by 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().
|
protected |
Definition at line 42 of file havoc_loops.cpp.
Referenced by get_modifies().
|
protected |
Definition at line 40 of file havoc_loops.cpp.
Referenced by havoc_loop().
|
protected |
Definition at line 41 of file havoc_loops.cpp.
Referenced by get_modifies().
|
protected |
Definition at line 43 of file havoc_loops.cpp.
Referenced by havoc_loops().