cprover
|
#include <path_symex_history.h>
Public Types | |
enum | kindt { NON_BRANCH, BRANCH_TAKEN, BRANCH_NOT_TAKEN } |
Public Member Functions | |
bool | is_branch_taken () const |
bool | is_branch_not_taken () const |
bool | is_branch () const |
path_symex_stept () | |
void | convert (decision_proceduret &dest) const |
void | output (std::ostream &) const |
Public Attributes | |
enum path_symex_stept::kindt | branch |
path_symex_step_reft | predecessor |
unsigned | thread_nr |
loc_reft | pc |
exprt | guard |
exprt | ssa_rhs |
exprt | full_lhs |
symbol_exprt | ssa_lhs |
bool | hidden |
Definition at line 77 of file path_symex_history.h.
Enumerator | |
---|---|
NON_BRANCH | |
BRANCH_TAKEN | |
BRANCH_NOT_TAKEN |
Definition at line 80 of file path_symex_history.h.
|
inline |
Definition at line 114 of file path_symex_history.h.
References convert().
void path_symex_stept::convert | ( | decision_proceduret & | dest | ) | const |
Definition at line 39 of file path_symex_history.cpp.
References guard, irept::is_not_nil(), ssa_lhs, and ssa_rhs.
Referenced by operator<<().
|
inline |
Definition at line 95 of file path_symex_history.h.
Referenced by path_symex_statet::last_was_branch().
|
inline |
Definition at line 90 of file path_symex_history.h.
|
inline |
Definition at line 85 of file path_symex_history.h.
void path_symex_stept::output | ( | std::ostream & | out | ) | const |
Definition at line 20 of file path_symex_history.cpp.
References from_expr(), full_lhs, guard, ssa_lhs, and ssa_rhs.
enum path_symex_stept::kindt path_symex_stept::branch |
Referenced by path_symext::do_goto().
exprt path_symex_stept::full_lhs |
Definition at line 109 of file path_symex_history.h.
Referenced by path_symext::assign_rec(), build_goto_trace(), and output().
exprt path_symex_stept::guard |
Definition at line 108 of file path_symex_history.h.
Referenced by path_symext::assign_rec(), convert(), path_symext::do_assert_fail(), path_symext::do_goto(), path_symext::function_call_rec(), path_symext::operator()(), and output().
bool path_symex_stept::hidden |
Definition at line 112 of file path_symex_history.h.
loc_reft path_symex_stept::pc |
Definition at line 106 of file path_symex_history.h.
Referenced by build_goto_trace(), and path_symex_statet::record_step().
path_symex_step_reft path_symex_stept::predecessor |
Definition at line 100 of file path_symex_history.h.
symbol_exprt path_symex_stept::ssa_lhs |
Definition at line 110 of file path_symex_history.h.
Referenced by path_symext::assign_rec(), build_goto_trace(), convert(), and output().
exprt path_symex_stept::ssa_rhs |
Definition at line 108 of file path_symex_history.h.
Referenced by path_symext::assign_rec(), convert(), and output().
unsigned path_symex_stept::thread_nr |
Definition at line 103 of file path_symex_history.h.
Referenced by build_goto_trace(), and path_symex_statet::record_step().