cprover
path_symex_step_reft Class Reference

#include <path_symex_history.h>

Collaboration diagram for path_symex_step_reft:
[legend]

Public Member Functions

 path_symex_step_reft (class path_symex_historyt &_history)
 
 path_symex_step_reft ()
 
bool is_nil () const
 
path_symex_historytget_history () const
 
path_symex_step_reftoperator-- ()
 
path_symex_steptoperator* () const
 
path_symex_steptoperator-> () const
 
void generate_successor ()
 
void build_history (std::vector< path_symex_step_reft > &dest) const
 

Protected Member Functions

path_symex_steptget () const
 

Protected Attributes

std::size_t index
 
class path_symex_historythistory
 

Detailed Description

Definition at line 28 of file path_symex_history.h.

Constructor & Destructor Documentation

§ path_symex_step_reft() [1/2]

path_symex_step_reft::path_symex_step_reft ( class path_symex_historyt _history)
inlineexplicit

Definition at line 31 of file path_symex_history.h.

§ path_symex_step_reft() [2/2]

path_symex_step_reft::path_symex_step_reft ( )
inline

Definition at line 38 of file path_symex_history.h.

Member Function Documentation

§ build_history()

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(), path_searcht::do_show_vcc(), and operator->().

§ generate_successor()

void path_symex_step_reft::generate_successor ( )
inline

§ get()

path_symex_stept & path_symex_step_reft::get ( ) const
inlineprotected

§ get_history()

path_symex_historyt& path_symex_step_reft::get_history ( ) const
inline

Definition at line 48 of file path_symex_history.h.

References history, INVARIANT_STRUCTURED, and operator--().

§ is_nil()

bool path_symex_step_reft::is_nil ( ) const
inline

§ operator*()

path_symex_stept& path_symex_step_reft::operator* ( ) const
inline

Definition at line 58 of file path_symex_history.h.

§ operator--()

path_symex_step_reft & path_symex_step_reft::operator-- ( )
inline

Definition at line 167 of file path_symex_history.h.

Referenced by get_history().

§ operator->()

path_symex_stept* path_symex_step_reft::operator-> ( ) const
inline

Definition at line 59 of file path_symex_history.h.

References build_history(), and generate_successor().

Member Data Documentation

§ history

class path_symex_historyt* path_symex_step_reft::history
protected

Definition at line 69 of file path_symex_history.h.

Referenced by generate_successor(), get(), and get_history().

§ index

std::size_t path_symex_step_reft::index
protected

Definition at line 68 of file path_symex_history.h.

Referenced by generate_successor(), get(), and is_nil().


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