cprover
slice.h File Reference

Slicer for symex traces. More...

#include "symex_target_equation.h"
#include <list>
Include dependency graph for slice.h:
This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Typedefs

typedef std::unordered_set< irep_idtsymbol_sett
 

Functions

void slice (symex_target_equationt &equation)
 
void simple_slice (symex_target_equationt &equation)
 
void slice (symex_target_equationt &equation, const std::list< exprt > &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...
 

Detailed Description

Slicer for symex traces.

Definition in file slice.h.

Typedef Documentation

◆ symbol_sett

typedef std::unordered_set<irep_idt> symbol_sett

Definition at line 32 of file slice.h.

Function Documentation

◆ collect_open_variables()

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

Parameters
equationsymex trace
open_variablestarget set
Returns
None. But open_variables is modified as a side-effect.

Definition at line 220 of file slice.cpp.

References symex_slicet::collect_open_variables().

◆ simple_slice()

void simple_slice ( symex_target_equationt equation)

Definition at line 240 of file slice.cpp.

References symex_target_equationt::SSA_steps.

Referenced by bmct::slice().

◆ slice() [1/2]

void slice ( symex_target_equationt equation)

Definition at line 209 of file slice.cpp.

References symex_slicet::slice().

Referenced by scratch_programt::check_sat().

◆ slice() [2/2]

void slice ( symex_target_equationt equation,
const std::list< exprt > &  expressions 
)

Slice the symex trace with respect to a list of expressions.

Parameters
equationsymex trace to be sliced
expressionlist of expressions, targets for slicing
Returns
None. But equation is modified as a side-effect.

Definition at line 232 of file slice.cpp.

References symex_slicet::slice().