cprover
|
Slicer for symex traces. More...
#include "symex_target_equation.h"
Go to the source code of this file.
Typedefs | |
typedef std::unordered_set< irep_idt, irep_id_hash > | symbol_sett |
Functions | |
void | slice (symex_target_equationt &equation) |
void | simple_slice (symex_target_equationt &equation) |
void | slice (symex_target_equationt &equation, const expr_listt &expressions) |
Slice the symex trace with respect to a list of expressions. More... | |
void | collect_open_variables (const symex_target_equationt &equation, symbol_sett &open_variables) |
Collect the open variables, i.e. More... | |
Slicer for symex traces.
Definition in file slice.h.
typedef std::unordered_set<irep_idt, irep_id_hash> symbol_sett |
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
equation | symex trace |
open_variables | target set |
Definition at line 220 of file slice.cpp.
References symex_slicet::collect_open_variables().
void simple_slice | ( | symex_target_equationt & | equation | ) |
Definition at line 239 of file slice.cpp.
References symex_target_equationt::SSA_steps.
Referenced by bmct::run().
void slice | ( | symex_target_equationt & | equation | ) |
Definition at line 209 of file slice.cpp.
References symex_slicet::slice().
Referenced by scratch_programt::check_sat(), and bmct::run().
void slice | ( | symex_target_equationt & | equation, |
const expr_listt & | expressions | ||
) |
Slice the symex trace with respect to a list of expressions.
equation | symex trace to be sliced |
expression | list of expressions, targets for slicing |
Definition at line 232 of file slice.cpp.
References symex_slicet::slice().