cprover
|
#include <symex_target_equation.h>
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 |
void | output (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 |
exprt | cond_expr |
literalt | cond_literal |
std::string | comment |
irep_idt | format_string |
irep_idt | io_id |
bool | formatted =false |
std::list< exprt > | io_args |
std::list< exprt > | converted_io_args |
irep_idt | identifier |
unsigned | atomic_section_id =0 |
bool | ignore =false |
Definition at line 170 of file symex_target_equation.h.
|
inline |
Definition at line 241 of file symex_target_equation.h.
|
inline |
Definition at line 177 of file symex_target_equation.h.
References goto_trace_stept::ASSERT, and type.
Referenced by output().
|
inline |
Definition at line 181 of file symex_target_equation.h.
References goto_trace_stept::ASSIGNMENT, and type.
Referenced by output().
|
inline |
Definition at line 179 of file symex_target_equation.h.
References goto_trace_stept::ASSUME, and type.
Referenced by output().
|
inline |
Definition at line 205 of file symex_target_equation.h.
References goto_trace_stept::ATOMIC_BEGIN, and type.
|
inline |
Definition at line 207 of file symex_target_equation.h.
References goto_trace_stept::ATOMIC_END, and type.
|
inline |
Definition at line 185 of file symex_target_equation.h.
References goto_trace_stept::CONSTRAINT, and type.
Referenced by output().
|
inline |
Definition at line 191 of file symex_target_equation.h.
References goto_trace_stept::DECL, and type.
|
inline |
Definition at line 193 of file symex_target_equation.h.
References goto_trace_stept::FUNCTION_CALL, and type.
Referenced by update_internal_field().
|
inline |
Definition at line 195 of file symex_target_equation.h.
References goto_trace_stept::FUNCTION_RETURN, and type.
|
inline |
Definition at line 183 of file symex_target_equation.h.
References goto_trace_stept::GOTO, and type.
|
inline |
Definition at line 187 of file symex_target_equation.h.
References goto_trace_stept::LOCATION, and type.
|
inline |
Definition at line 203 of file symex_target_equation.h.
References goto_trace_stept::MEMORY_BARRIER, and type.
|
inline |
Definition at line 189 of file symex_target_equation.h.
References goto_trace_stept::OUTPUT, and type.
|
inline |
Definition at line 197 of file symex_target_equation.h.
References goto_trace_stept::SHARED_READ, and type.
Referenced by output().
|
inline |
Definition at line 199 of file symex_target_equation.h.
References goto_trace_stept::SHARED_WRITE, and type.
Referenced by output().
|
inline |
Definition at line 201 of file symex_target_equation.h.
References goto_trace_stept::SPAWN, and type.
void symex_target_equationt::SSA_stept::output | ( | const namespacet & | ns, |
std::ostream & | out | ||
) | const |
Definition at line 722 of file symex_target_equation.cpp.
References goto_trace_stept::ASSERT, goto_trace_stept::ASSIGNMENT, assignment_type, goto_trace_stept::ASSUME, goto_trace_stept::ATOMIC_BEGIN, goto_trace_stept::ATOMIC_END, comment, cond_expr, goto_trace_stept::CONSTRAINT, goto_trace_stept::DEAD, goto_trace_stept::DECL, from_expr(), goto_trace_stept::FUNCTION_CALL, goto_trace_stept::FUNCTION_RETURN, goto_trace_stept::GOTO, symex_targett::GUARD, guard, symex_targett::HIDDEN, symex_targett::HIDDEN_ACTUAL_PARAMETER, goto_trace_stept::INPUT, is_assert(), is_assignment(), is_assume(), is_constraint(), is_shared_read(), is_shared_write(), goto_trace_stept::LOCATION, goto_trace_stept::MEMORY_BARRIER, goto_trace_stept::OUTPUT, symex_targett::PHI, goto_trace_stept::SHARED_READ, goto_trace_stept::SHARED_WRITE, source, goto_trace_stept::SPAWN, ssa_lhs, symex_targett::STATE, type, UNREACHABLE, and symex_targett::VISIBLE_ACTUAL_PARAMETER.
Referenced by equation_conversion_exceptiont::equation_conversion_exceptiont().
void symex_target_equationt::SSA_stept::output | ( | std::ostream & | out | ) | const |
Definition at line 825 of file symex_target_equation.cpp.
References goto_trace_stept::ASSERT, goto_trace_stept::ASSIGNMENT, goto_trace_stept::ASSUME, goto_trace_stept::ATOMIC_BEGIN, goto_trace_stept::ATOMIC_END, comment(), goto_trace_stept::CONSTRAINT, goto_trace_stept::DEAD, goto_trace_stept::DECL, format(), goto_trace_stept::FUNCTION_CALL, goto_trace_stept::FUNCTION_RETURN, goto_trace_stept::GOTO, symex_targett::GUARD, symex_targett::HIDDEN, symex_targett::HIDDEN_ACTUAL_PARAMETER, goto_trace_stept::INPUT, goto_trace_stept::LOCATION, goto_trace_stept::MEMORY_BARRIER, goto_trace_stept::OUTPUT, symex_targett::PHI, goto_trace_stept::SHARED_READ, goto_trace_stept::SHARED_WRITE, goto_trace_stept::SPAWN, symex_targett::STATE, UNREACHABLE, and symex_targett::VISIBLE_ACTUAL_PARAMETER.
assignment_typet symex_target_equationt::SSA_stept::assignment_type |
Definition at line 219 of file symex_target_equation.h.
Referenced by symex_slice_by_tracet::assign_merges(), symex_target_equationt::assignment(), build_goto_trace(), and output().
unsigned symex_target_equationt::SSA_stept::atomic_section_id =0 |
Definition at line 236 of file symex_target_equation.h.
Referenced by partial_order_concurrencyt::add_init_writes(), symex_target_equationt::atomic_begin(), symex_target_equationt::atomic_end(), symex_target_equationt::shared_read(), and symex_target_equationt::shared_write().
std::string symex_target_equationt::SSA_stept::comment |
Definition at line 224 of file symex_target_equation.h.
Referenced by symex_target_equationt::assertion(), symex_target_equationt::constraint(), and output().
exprt symex_target_equationt::SSA_stept::cond_expr |
Definition at line 222 of file symex_target_equation.h.
Referenced by symex_target_equationt::assertion(), symex_slice_by_tracet::assign_merges(), symex_target_equationt::assignment(), symex_target_equationt::assumption(), symex_slicet::collect_open_variables(), symex_target_equationt::constraint(), symex_target_equationt::decl(), symex_target_equationt::goto_instruction(), symex_target_equationt::merge_ireps(), output(), symex_slicet::slice(), and symex_slice_by_tracet::slice_by_trace().
literalt symex_target_equationt::SSA_stept::cond_literal |
Definition at line 223 of file symex_target_equation.h.
std::list<exprt> symex_target_equationt::SSA_stept::converted_io_args |
Definition at line 230 of file symex_target_equation.h.
irep_idt symex_target_equationt::SSA_stept::format_string |
Definition at line 227 of file symex_target_equation.h.
Referenced by symex_target_equationt::output_fmt().
bool symex_target_equationt::SSA_stept::formatted =false |
Definition at line 228 of file symex_target_equation.h.
Referenced by symex_target_equationt::output_fmt().
exprt symex_target_equationt::SSA_stept::guard |
Definition at line 212 of file symex_target_equation.h.
Referenced by partial_order_concurrencyt::add_init_writes(), symex_target_equationt::assertion(), symex_slice_by_tracet::assign_merges(), symex_target_equationt::assignment(), symex_target_equationt::assumption(), symex_target_equationt::atomic_begin(), symex_target_equationt::atomic_end(), symex_slicet::collect_open_variables(), symex_target_equationt::constraint(), symex_target_equationt::decl(), symex_target_equationt::function_call(), symex_target_equationt::function_return(), symex_target_equationt::goto_instruction(), symex_target_equationt::input(), symex_target_equationt::location(), symex_target_equationt::memory_barrier(), symex_target_equationt::merge_ireps(), symex_target_equationt::output(), output(), symex_target_equationt::output_fmt(), symex_target_equationt::shared_read(), symex_target_equationt::shared_write(), symex_slicet::slice(), symex_slice_by_tracet::slice_by_trace(), and symex_target_equationt::spawn().
literalt symex_target_equationt::SSA_stept::guard_literal |
Definition at line 213 of file symex_target_equation.h.
Referenced by build_goto_trace().
bool symex_target_equationt::SSA_stept::hidden =false |
Definition at line 210 of file symex_target_equation.h.
Referenced by symex_target_equationt::assignment(), and symex_target_equationt::decl().
irep_idt symex_target_equationt::SSA_stept::identifier |
Definition at line 233 of file symex_target_equation.h.
Referenced by symex_target_equationt::function_call(), and symex_target_equationt::function_return().
bool symex_target_equationt::SSA_stept::ignore =false |
Definition at line 239 of file symex_target_equation.h.
Referenced by symex_slicet::slice_assignment(), and symex_slicet::slice_decl().
std::list<exprt> symex_target_equationt::SSA_stept::io_args |
Definition at line 229 of file symex_target_equation.h.
Referenced by symex_target_equationt::input(), symex_target_equationt::merge_ireps(), symex_target_equationt::output(), and symex_target_equationt::output_fmt().
irep_idt symex_target_equationt::SSA_stept::io_id |
Definition at line 227 of file symex_target_equation.h.
Referenced by symex_target_equationt::input(), symex_target_equationt::output(), and symex_target_equationt::output_fmt().
exprt symex_target_equationt::SSA_stept::original_full_lhs |
Definition at line 217 of file symex_target_equation.h.
Referenced by symex_target_equationt::assignment(), symex_target_equationt::decl(), and symex_target_equationt::merge_ireps().
sourcet symex_target_equationt::SSA_stept::source |
Definition at line 173 of file symex_target_equation.h.
Referenced by partial_order_concurrencyt::add_init_writes(), symex_target_equationt::assertion(), symex_slice_by_tracet::assign_merges(), symex_target_equationt::assignment(), symex_target_equationt::assumption(), symex_target_equationt::atomic_begin(), symex_target_equationt::atomic_end(), symex_target_equationt::constraint(), symex_target_equationt::decl(), equation_conversion_exceptiont::equation_conversion_exceptiont(), symex_target_equationt::function_call(), symex_target_equationt::function_return(), symex_target_equationt::goto_instruction(), symex_target_equationt::input(), symex_target_equationt::location(), symex_target_equationt::memory_barrier(), symex_target_equationt::output(), output(), symex_target_equationt::output_fmt(), symex_target_equationt::shared_read(), symex_target_equationt::shared_write(), symex_slice_by_tracet::slice_by_trace(), symex_target_equationt::spawn(), and update_internal_field().
exprt symex_target_equationt::SSA_stept::ssa_full_lhs |
Definition at line 217 of file symex_target_equation.h.
Referenced by symex_target_equationt::assignment(), symex_target_equationt::decl(), and symex_target_equationt::merge_ireps().
ssa_exprt symex_target_equationt::SSA_stept::ssa_lhs |
Definition at line 216 of file symex_target_equation.h.
Referenced by partial_order_concurrencyt::add_init_writes(), symex_slice_by_tracet::assign_merges(), symex_target_equationt::assignment(), symex_slicet::collect_open_variables(), preconditiont::compute_rec(), symex_target_equationt::decl(), symex_target_equationt::merge_ireps(), output(), symex_target_equationt::shared_read(), symex_target_equationt::shared_write(), symex_slicet::slice_assignment(), symex_slice_by_tracet::slice_by_trace(), symex_slicet::slice_decl(), postconditiont::strengthen(), update_internal_field(), and postconditiont::weaken().
exprt symex_target_equationt::SSA_stept::ssa_rhs |
Definition at line 218 of file symex_target_equation.h.
Referenced by symex_slice_by_tracet::assign_merges(), symex_target_equationt::assignment(), symex_slicet::collect_open_variables(), preconditiont::compute_rec(), symex_target_equationt::merge_ireps(), symex_slicet::slice_assignment(), postconditiont::strengthen(), and update_internal_field().
goto_trace_stept::typet symex_target_equationt::SSA_stept::type |
Definition at line 174 of file symex_target_equation.h.
Referenced by partial_order_concurrencyt::add_init_writes(), symex_target_equationt::assertion(), symex_slice_by_tracet::assign_merges(), symex_target_equationt::assignment(), symex_target_equationt::assumption(), symex_target_equationt::atomic_begin(), symex_target_equationt::atomic_end(), symex_slicet::collect_open_variables(), symex_target_equationt::constraint(), symex_target_equationt::decl(), symex_target_equationt::function_call(), symex_target_equationt::function_return(), symex_target_equationt::goto_instruction(), symex_target_equationt::input(), is_assert(), is_assignment(), is_assume(), is_atomic_begin(), is_atomic_end(), is_constraint(), is_decl(), is_function_call(), is_function_return(), is_goto(), is_location(), is_memory_barrier(), is_output(), is_shared_read(), is_shared_write(), is_spawn(), symex_target_equationt::location(), symex_target_equationt::memory_barrier(), symex_target_equationt::output(), output(), symex_target_equationt::output_fmt(), symex_target_equationt::shared_read(), symex_target_equationt::shared_write(), symex_slicet::slice(), symex_slice_by_tracet::slice_by_trace(), and symex_target_equationt::spawn().