symex_target_equationt::SSA_stept Class Reference

#include <symex_target_equation.h>

Classes
struct	output_datat

Public Member Functions
bool	is_assert () const
bool	is_assume () const
bool	is_assignment () const
bool	is_output () const
bool	is_renumber () const
bool	is_skip () const
bool	is_branching () const
	SSA_stept ()
	SSA_stept (const SSA_stept &o)
SSA_stept &	operator= (const SSA_stept &o)
	SSA_stept (SSA_stept &&)=default
SSA_stept &	operator= (SSA_stept &&)=default
output_datat &	output_payload ()
const std::vector< stack_framet > &	stack_trace () const
std::vector< stack_framet > &	stack_trace_payload ()
void	output (const namespacet &ns, std::ostream &out) const
void	short_output (const namespacet &ns, std::ostream &out, bool show_ignored=false) const
void	dump () const

Public Attributes
sourcet	source
symex_targett::step_typet	type
expr2tc	guard
expr2tc	lhs
expr2tc	rhs
expr2tc	original_lhs
expr2tc	original_rhs
expr2tc	cond
expr2tc	cond_neg
	cond with the claim negated under the same guards (issue #7585).
irep_idt	comment
std::unique_ptr< output_datat >	output_data
std::unique_ptr< std::vector< stack_framet > >	stack_trace_box
expr2tc	cond_expr
bool	ignore
bool	hidden
unsigned	loop_number

Constructor & Destructor Documentation

SSA_stept() [1/3]

symex_target_equationt::SSA_stept::SSA_stept ( )

inline

SSA_stept() [2/3]

symex_target_equationt::SSA_stept::SSA_stept ( const SSA_stept & o )

inline

SSA_stept() [3/3]

symex_target_equationt::SSA_stept::SSA_stept ( SSA_stept && )

default

Member Function Documentation

dump()

void symex_target_equationt::SSA_stept::dump

(

)

const

is_assert()

bool symex_target_equationt::SSA_stept::is_assert ( ) const

inline

is_assignment()

bool symex_target_equationt::SSA_stept::is_assignment ( ) const

inline

is_assume()

bool symex_target_equationt::SSA_stept::is_assume ( ) const

inline

is_branching()

bool symex_target_equationt::SSA_stept::is_branching ( ) const

inline

is_output()

bool symex_target_equationt::SSA_stept::is_output ( ) const

inline

is_renumber()

bool symex_target_equationt::SSA_stept::is_renumber ( ) const

inline

is_skip()

bool symex_target_equationt::SSA_stept::is_skip ( ) const

inline

operator=() [1/2]

SSA_stept & symex_target_equationt::SSA_stept::operator= ( const SSA_stept & o )

inline

operator=() [2/2]

SSA_stept & symex_target_equationt::SSA_stept::operator= ( SSA_stept && )

default

output()

void symex_target_equationt::SSA_stept::output	(	const namespacet &	ns,
		std::ostream &	out ) const

output_payload()

output_datat & symex_target_equationt::SSA_stept::output_payload ( )

inline

short_output()

void symex_target_equationt::SSA_stept::short_output	(	const namespacet &	ns,
		std::ostream &	out,
		bool	show_ignored = false ) const

stack_trace()

const std::vector< stack_framet > & symex_target_equationt::SSA_stept::stack_trace ( ) const

inline

stack_trace_payload()

std::vector< stack_framet > & symex_target_equationt::SSA_stept::stack_trace_payload ( )

inline

Member Data Documentation

comment

irep_idt symex_target_equationt::SSA_stept::comment

cond

expr2tc symex_target_equationt::SSA_stept::cond

cond_expr

expr2tc symex_target_equationt::SSA_stept::cond_expr

cond_neg

expr2tc symex_target_equationt::SSA_stept::cond_neg

cond with the claim negated under the same guards (issue #7585).

guard

expr2tc symex_target_equationt::SSA_stept::guard

hidden

bool symex_target_equationt::SSA_stept::hidden

ignore

bool symex_target_equationt::SSA_stept::ignore

lhs

expr2tc symex_target_equationt::SSA_stept::lhs

loop_number

unsigned symex_target_equationt::SSA_stept::loop_number

original_lhs

expr2tc symex_target_equationt::SSA_stept::original_lhs

original_rhs

expr2tc symex_target_equationt::SSA_stept::original_rhs

output_data

std::unique_ptr<output_datat> symex_target_equationt::SSA_stept::output_data

rhs

expr2tc symex_target_equationt::SSA_stept::rhs

source

sourcet symex_target_equationt::SSA_stept::source

stack_trace_box

std::unique_ptr<std::vector<stack_framet> > symex_target_equationt::SSA_stept::stack_trace_box

type

symex_targett::step_typet symex_target_equationt::SSA_stept::type

---

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

• src/goto-symex/equation/symex_target_equation.h
• src/goto-symex/equation/symex_target_equation.cpp