cprover
Loading...
Searching...
No Matches
SSA_assignment_stept Class Reference

#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.

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< exprtio_args
std::list< exprtconverted_io_args
irep_idt called_function
std::vector< exprtssa_function_arguments
std::vector< exprtconverted_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::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: