path_symex_stept Class Reference

#include <path_symex_history.h>

Collaboration diagram for path_symex_stept:

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

Detailed Description

Definition at line 77 of file path_symex_history.h.

Member Enumeration Documentation

kindt

enum path_symex_stept::kindt

Enumerator
NON_BRANCH
BRANCH_TAKEN
BRANCH_NOT_TAKEN

Definition at line 80 of file path_symex_history.h.

Constructor & Destructor Documentation

path_symex_stept()

path_symex_stept::path_symex_stept ( )

inline

Definition at line 114 of file path_symex_history.h.

Member Function Documentation

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

is_branch()

bool path_symex_stept::is_branch ( ) const

inline

Definition at line 95 of file path_symex_history.h.

References branch, BRANCH_NOT_TAKEN, and BRANCH_TAKEN.

Referenced by path_symex_statet::last_was_branch().

is_branch_not_taken()

bool path_symex_stept::is_branch_not_taken ( ) const

inline

Definition at line 90 of file path_symex_history.h.

References branch, and BRANCH_NOT_TAKEN.

is_branch_taken()

bool path_symex_stept::is_branch_taken ( ) const

inline

Definition at line 85 of file path_symex_history.h.

References branch, and BRANCH_TAKEN.

output()

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.

Member Data Documentation

branch

enum path_symex_stept::kindt path_symex_stept::branch

Referenced by path_symext::do_goto(), is_branch(), is_branch_not_taken(), and is_branch_taken().

full_lhs

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

guard

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

hidden

bool path_symex_stept::hidden

Definition at line 112 of file path_symex_history.h.

pc

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

predecessor

path_symex_step_reft path_symex_stept::predecessor

Definition at line 100 of file path_symex_history.h.

ssa_lhs

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

ssa_rhs

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

thread_nr

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

---

The documentation for this class was generated from the following files:

• path-symex/path_symex_history.h
• path-symex/path_symex_history.cpp