cprover
|
#include <symex_slice_class.h>
Public Member Functions | |
void | slice (symex_target_equationt &equation) |
void | slice (symex_target_equationt &, const std::list< exprt > &) |
void | collect_open_variables (const symex_target_equationt &equation, symbol_sett &open_variables) |
Collect the open variables, i.e., variables that are used in RHS but never written in LHS. More... | |
Protected Member Functions | |
void | get_symbols (const exprt &expr) |
void | get_symbols (const typet &type) |
void | slice (symex_target_equationt::SSA_stept &SSA_step) |
void | slice_assignment (symex_target_equationt::SSA_stept &SSA_step) |
void | slice_decl (symex_target_equationt::SSA_stept &SSA_step) |
Protected Attributes | |
symbol_sett | depends |
Definition at line 18 of file symex_slice_class.h.
void symex_slicet::collect_open_variables | ( | const symex_target_equationt & | equation, |
symbol_sett & | open_variables | ||
) |
Collect the open variables, i.e., variables that are used in RHS but never written in LHS.
equation | symex trace |
open_variables | target set |
Definition at line 145 of file slice.cpp.
References goto_trace_stept::ASSERT, goto_trace_stept::ASSIGNMENT, goto_trace_stept::ASSUME, goto_trace_stept::ATOMIC_BEGIN, goto_trace_stept::ATOMIC_END, symex_target_equationt::SSA_stept::cond_expr, goto_trace_stept::CONSTRAINT, goto_trace_stept::DEAD, goto_trace_stept::DECL, depends, goto_trace_stept::FUNCTION_CALL, goto_trace_stept::FUNCTION_RETURN, symbol_exprt::get_identifier(), get_symbols(), symex_target_equationt::SSA_stept::guard, goto_trace_stept::INPUT, goto_trace_stept::LOCATION, goto_trace_stept::MEMORY_BARRIER, goto_trace_stept::NONE, goto_trace_stept::OUTPUT, goto_trace_stept::SHARED_READ, goto_trace_stept::SHARED_WRITE, goto_trace_stept::SPAWN, symex_target_equationt::SSA_stept::ssa_lhs, symex_target_equationt::SSA_stept::ssa_rhs, symex_target_equationt::SSA_steps, symex_target_equationt::SSA_stept::type, and UNREACHABLE.
Referenced by collect_open_variables().
|
protected |
Definition at line 18 of file slice.cpp.
References depends, forall_operands, irept::id(), to_symbol_expr(), and exprt::type().
Referenced by collect_open_variables(), slice(), and slice_assignment().
|
protected |
void symex_slicet::slice | ( | symex_target_equationt & | equation | ) |
Definition at line 45 of file slice.cpp.
References symex_target_equationt::SSA_steps.
void symex_slicet::slice | ( | symex_target_equationt & | equation, |
const std::list< exprt > & | exprs | ||
) |
Definition at line 34 of file slice.cpp.
References get_symbols(), and slice().
|
protected |
Definition at line 54 of file slice.cpp.
References goto_trace_stept::ASSERT, goto_trace_stept::ASSIGNMENT, goto_trace_stept::ASSUME, goto_trace_stept::ATOMIC_BEGIN, goto_trace_stept::ATOMIC_END, symex_target_equationt::SSA_stept::cond_expr, goto_trace_stept::CONSTRAINT, goto_trace_stept::DEAD, goto_trace_stept::DECL, goto_trace_stept::FUNCTION_CALL, goto_trace_stept::FUNCTION_RETURN, get_symbols(), goto_trace_stept::GOTO, symex_target_equationt::SSA_stept::guard, goto_trace_stept::INPUT, goto_trace_stept::LOCATION, goto_trace_stept::MEMORY_BARRIER, goto_trace_stept::OUTPUT, goto_trace_stept::SHARED_READ, goto_trace_stept::SHARED_WRITE, slice_assignment(), slice_decl(), goto_trace_stept::SPAWN, symex_target_equationt::SSA_stept::type, and UNREACHABLE.
|
protected |
Definition at line 112 of file slice.cpp.
References depends, symbol_exprt::get_identifier(), get_symbols(), irept::id(), symex_target_equationt::SSA_stept::ignore, symex_target_equationt::SSA_stept::ssa_lhs, and symex_target_equationt::SSA_stept::ssa_rhs.
Referenced by slice().
|
protected |
Definition at line 127 of file slice.cpp.
References depends, symbol_exprt::get_identifier(), irept::id(), symex_target_equationt::SSA_stept::ignore, and symex_target_equationt::SSA_stept::ssa_lhs.
Referenced by slice().
|
protected |
Definition at line 30 of file symex_slice_class.h.
Referenced by collect_open_variables(), get_symbols(), slice_assignment(), and slice_decl().