cprover
path_symex_stept Class Reference

#include <path_symex_history.h>

Collaboration diagram for path_symex_stept:
[legend]

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

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.

References convert().

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.

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.

§ is_branch_taken()

bool path_symex_stept::is_branch_taken ( ) const
inline

Definition at line 85 of file path_symex_history.h.

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

§ 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

§ 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: