goto_trace_stept Class Reference

#include <goto_trace.h>

Public Member Functions
bool	is_assignment () const
bool	is_assume () const
bool	is_assert () const
bool	is_output () const
bool	is_skip () const
bool	is_renumber () const
bool	is_branching () const
void	output (const class namespacet &ns, std::ostream &out) const
void	dump () const
	goto_trace_stept ()

Public Attributes
unsigned	step_nr
std::vector< stack_framet >	stack_trace
symex_targett::step_typet	type
goto_programt::const_targett	pc
unsigned	thread_nr
bool	guard
std::string	comment
expr2tc	lhs
expr2tc	rhs
expr2tc	value
expr2tc	original_lhs
std::list< std::pair< expr2tc, expr2tc > >	nondet_reads
std::string	format_string
std::list< expr2tc >	output_args

Constructor & Destructor Documentation

goto_trace_stept()

goto_trace_stept::goto_trace_stept ( )

inline

Member Function Documentation

dump()

void goto_trace_stept::dump

(

)

const

is_assert()

bool goto_trace_stept::is_assert ( ) const

inline

is_assignment()

bool goto_trace_stept::is_assignment ( ) const

inline

is_assume()

bool goto_trace_stept::is_assume ( ) const

inline

is_branching()

bool goto_trace_stept::is_branching ( ) const

inline

is_output()

bool goto_trace_stept::is_output ( ) const

inline

is_renumber()

bool goto_trace_stept::is_renumber ( ) const

inline

is_skip()

bool goto_trace_stept::is_skip ( ) const

inline

output()

void goto_trace_stept::output	(	const class namespacet &	ns,
		std::ostream &	out ) const

Member Data Documentation

comment

std::string goto_trace_stept::comment

format_string

std::string goto_trace_stept::format_string

guard

bool goto_trace_stept::guard

lhs

expr2tc goto_trace_stept::lhs

nondet_reads

std::list<std::pair<expr2tc, expr2tc> > goto_trace_stept::nondet_reads

original_lhs

expr2tc goto_trace_stept::original_lhs

output_args

std::list<expr2tc> goto_trace_stept::output_args

pc

goto_programt::const_targett goto_trace_stept::pc

rhs

expr2tc goto_trace_stept::rhs

stack_trace

std::vector<stack_framet> goto_trace_stept::stack_trace

step_nr

unsigned goto_trace_stept::step_nr

thread_nr

unsigned goto_trace_stept::thread_nr

type

symex_targett::step_typet goto_trace_stept::type

value

expr2tc goto_trace_stept::value

---

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

• src/goto-symex/trace/goto_trace.h
• src/goto-symex/trace/goto_trace.cpp