#include <ssa_step.h>

Inheritance diagram for SSA_assignment_stept:

Collaboration diagram for SSA_assignment_stept:

Public Member Functions
	SSA_assignment_stept (symex_targett::sourcet source, exprt guard, ssa_exprt ssa_lhs, exprt ssa_full_lhs, exprt original_full_lhs, exprt ssa_rhs, symex_targett::assignment_typet assignment_type)

Public Member Functions inherited from SSA_stept
bool	is_assert () const

bool	is_assume () const

bool	is_assignment () const

bool	is_goto () const

bool	is_constraint () const

bool	is_location () const

bool	is_output () const

bool	is_decl () const

bool	is_function_call () const

bool	is_function_return () const

bool	is_shared_read () const

bool	is_shared_write () const

bool	is_spawn () const

bool	is_memory_barrier () const

bool	is_atomic_begin () const

bool	is_atomic_end () const

exprt	get_ssa_expr () const

	SSA_stept (const symex_targett::sourcet &_source, goto_trace_stept::typet _type)

void	output (std::ostream &out) const

void	validate (const namespacet &ns, const validation_modet vm) const
	Check that the SSA step is well-formed. More...

Additional Inherited Members
Public Attributes inherited from SSA_stept
symex_targett::sourcet	source

goto_trace_stept::typet	type

bool	hidden = false

exprt	guard

exprt	guard_handle

ssa_exprt	ssa_lhs

exprt	ssa_full_lhs

exprt	original_full_lhs

exprt	ssa_rhs

symex_targett::assignment_typet	assignment_type

exprt	cond_expr

exprt	cond_handle

std::string	comment

irep_idt	property_id

irep_idt	format_string

irep_idt	io_id

bool	formatted = false

std::list< exprt >	io_args

std::list< exprt >	converted_io_args

irep_idt	called_function

std::vector< exprt >	ssa_function_arguments

std::vector< exprt >	converted_function_arguments

unsigned	atomic_section_id = 0

bool	ignore = false

bool	converted = false

Detailed Description

Definition at line 203 of file ssa_step.h.

Constructor & Destructor Documentation

SSA_assignment_stept::SSA_assignment_stept	(	symex_targett::sourcet	source,
		exprt	guard,
		ssa_exprt	ssa_lhs,
		exprt	ssa_full_lhs,
		exprt	original_full_lhs,
		exprt	ssa_rhs,
		symex_targett::assignment_typet	assignment_type
	)

Definition at line 189 of file ssa_step.cpp.

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