cprover
|
#include <path_symex_history.h>
Public Member Functions | |
path_symex_step_reft (class path_symex_historyt &_history) | |
path_symex_step_reft () | |
bool | is_nil () const |
path_symex_historyt & | get_history () const |
path_symex_step_reft & | operator-- () |
path_symex_stept & | operator* () const |
path_symex_stept * | operator-> () const |
void | generate_successor () |
void | build_history (std::vector< path_symex_step_reft > &dest) const |
Protected Member Functions | |
path_symex_stept & | get () const |
Protected Attributes | |
std::size_t | index |
class path_symex_historyt * | history |
Definition at line 28 of file path_symex_history.h.
|
inlineexplicit |
Definition at line 31 of file path_symex_history.h.
|
inline |
Definition at line 38 of file path_symex_history.h.
void path_symex_step_reft::build_history | ( | std::vector< path_symex_step_reft > & | dest | ) | const |
Definition at line 48 of file path_symex_history.cpp.
References is_nil().
Referenced by build_goto_trace(), and path_searcht::do_show_vcc().
|
inline |
Definition at line 157 of file path_symex_history.h.
References history, index, INVARIANT_STRUCTURED, and path_symex_historyt::step_container.
Referenced by path_symex_statet::record_step().
|
inlineprotected |
Definition at line 173 of file path_symex_history.h.
References history, index, INVARIANT_STRUCTURED, is_nil(), and path_symex_historyt::step_container.
|
inline |
Definition at line 48 of file path_symex_history.h.
References history, and INVARIANT_STRUCTURED.
|
inline |
Definition at line 43 of file path_symex_history.h.
References index.
Referenced by build_history(), get(), get_branches(), path_symex_statet::last_was_branch(), operator<<(), and path_symex_statet::record_step().
|
inline |
Definition at line 58 of file path_symex_history.h.
|
inline |
Definition at line 167 of file path_symex_history.h.
|
inline |
Definition at line 59 of file path_symex_history.h.
|
protected |
Definition at line 69 of file path_symex_history.h.
Referenced by generate_successor(), get(), and get_history().
|
protected |
Definition at line 68 of file path_symex_history.h.
Referenced by generate_successor(), get(), and is_nil().