cprover
symex_target_equationt::SSA_stept Class Reference

#include <symex_target_equation.h>

Collaboration diagram for symex_target_equationt::SSA_stept:
[legend]

Public Member Functions

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
 
 SSA_stept ()
 
void output (const namespacet &ns, std::ostream &out) const
 

Public Attributes

sourcet source
 
goto_trace_stept::typet type
 
bool hidden =false
 
exprt guard
 
literalt guard_literal
 
ssa_exprt ssa_lhs
 
exprt ssa_full_lhs
 
exprt original_full_lhs
 
exprt ssa_rhs
 
assignment_typet assignment_type =assignment_typet::STATE
 
exprt cond_expr
 
literalt cond_literal
 
std::string comment
 
irep_idt format_string
 
irep_idt io_id
 
bool formatted =false
 
std::list< exprtio_args
 
std::list< exprtconverted_io_args
 
irep_idt identifier
 
unsigned atomic_section_id =0
 
bool ignore =false
 

Detailed Description

Definition at line 170 of file symex_target_equation.h.

Constructor & Destructor Documentation

◆ SSA_stept()

symex_target_equationt::SSA_stept::SSA_stept ( )
inline

Definition at line 241 of file symex_target_equation.h.

Member Function Documentation

◆ is_assert()

bool symex_target_equationt::SSA_stept::is_assert ( ) const
inline

Definition at line 177 of file symex_target_equation.h.

References goto_trace_stept::ASSERT, and type.

Referenced by build_goto_trace(), and output().

◆ is_assignment()

bool symex_target_equationt::SSA_stept::is_assignment ( ) const
inline

Definition at line 181 of file symex_target_equation.h.

References goto_trace_stept::ASSIGNMENT, and type.

Referenced by output().

◆ is_assume()

bool symex_target_equationt::SSA_stept::is_assume ( ) const
inline

Definition at line 179 of file symex_target_equation.h.

References goto_trace_stept::ASSUME, and type.

Referenced by build_goto_trace(), and output().

◆ is_atomic_begin()

bool symex_target_equationt::SSA_stept::is_atomic_begin ( ) const
inline

Definition at line 205 of file symex_target_equation.h.

References goto_trace_stept::ATOMIC_BEGIN, and type.

◆ is_atomic_end()

bool symex_target_equationt::SSA_stept::is_atomic_end ( ) const
inline

Definition at line 207 of file symex_target_equation.h.

References goto_trace_stept::ATOMIC_END, and type.

◆ is_constraint()

bool symex_target_equationt::SSA_stept::is_constraint ( ) const
inline

Definition at line 185 of file symex_target_equation.h.

References goto_trace_stept::CONSTRAINT, and type.

Referenced by output().

◆ is_decl()

bool symex_target_equationt::SSA_stept::is_decl ( ) const
inline

Definition at line 191 of file symex_target_equation.h.

References goto_trace_stept::DECL, and type.

◆ is_function_call()

bool symex_target_equationt::SSA_stept::is_function_call ( ) const
inline

Definition at line 193 of file symex_target_equation.h.

References goto_trace_stept::FUNCTION_CALL, and type.

◆ is_function_return()

bool symex_target_equationt::SSA_stept::is_function_return ( ) const
inline

Definition at line 195 of file symex_target_equation.h.

References goto_trace_stept::FUNCTION_RETURN, and type.

◆ is_goto()

bool symex_target_equationt::SSA_stept::is_goto ( ) const
inline

Definition at line 183 of file symex_target_equation.h.

References goto_trace_stept::GOTO, and type.

Referenced by build_goto_trace().

◆ is_location()

bool symex_target_equationt::SSA_stept::is_location ( ) const
inline

Definition at line 187 of file symex_target_equation.h.

References goto_trace_stept::LOCATION, and type.

◆ is_memory_barrier()

bool symex_target_equationt::SSA_stept::is_memory_barrier ( ) const
inline

Definition at line 203 of file symex_target_equation.h.

References goto_trace_stept::MEMORY_BARRIER, and type.

◆ is_output()

bool symex_target_equationt::SSA_stept::is_output ( ) const
inline

Definition at line 189 of file symex_target_equation.h.

References goto_trace_stept::OUTPUT, and type.

◆ is_shared_read()

bool symex_target_equationt::SSA_stept::is_shared_read ( ) const
inline

Definition at line 197 of file symex_target_equation.h.

References goto_trace_stept::SHARED_READ, and type.

Referenced by output().

◆ is_shared_write()

bool symex_target_equationt::SSA_stept::is_shared_write ( ) const
inline

Definition at line 199 of file symex_target_equation.h.

References goto_trace_stept::SHARED_WRITE, and type.

Referenced by output().

◆ is_spawn()

bool symex_target_equationt::SSA_stept::is_spawn ( ) const
inline

Definition at line 201 of file symex_target_equation.h.

References goto_trace_stept::SPAWN, and type.

◆ output()

Member Data Documentation

◆ assignment_type

assignment_typet symex_target_equationt::SSA_stept::assignment_type =assignment_typet::STATE

◆ atomic_section_id

◆ comment

std::string symex_target_equationt::SSA_stept::comment

◆ cond_expr

◆ cond_literal

literalt symex_target_equationt::SSA_stept::cond_literal

Definition at line 223 of file symex_target_equation.h.

Referenced by build_goto_trace().

◆ converted_io_args

std::list<exprt> symex_target_equationt::SSA_stept::converted_io_args

Definition at line 230 of file symex_target_equation.h.

Referenced by build_goto_trace().

◆ format_string

irep_idt symex_target_equationt::SSA_stept::format_string

◆ formatted

bool symex_target_equationt::SSA_stept::formatted =false

◆ guard

◆ guard_literal

literalt symex_target_equationt::SSA_stept::guard_literal

Definition at line 213 of file symex_target_equation.h.

Referenced by build_goto_trace().

◆ hidden

bool symex_target_equationt::SSA_stept::hidden =false

◆ identifier

irep_idt symex_target_equationt::SSA_stept::identifier

◆ ignore

bool symex_target_equationt::SSA_stept::ignore =false

◆ io_args

std::list<exprt> symex_target_equationt::SSA_stept::io_args

◆ io_id

◆ original_full_lhs

exprt symex_target_equationt::SSA_stept::original_full_lhs

◆ source

◆ ssa_full_lhs

exprt symex_target_equationt::SSA_stept::ssa_full_lhs

◆ ssa_lhs

◆ ssa_rhs

◆ type


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