Loading...

Searching...

No Matches

Typedefs | Functions

slice.h File Reference

Slicer for symex traces. More...

#include <list>
#include <unordered_set>
#include <util/irep.h>

+ 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_idt > symbol_sett

Functions

void slice (symex_target_equationt &equation)

void revert_slice (symex_target_equationt &)

Undo whatever has been done by slice

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.

void collect_open_variables (const symex_target_equationt &equation, symbol_sett &open_variables)

Collect the open variables, i.e.

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 39 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: equation symex trace

[out] open_variables target set

Definition at line 215 of file slice.cpp.

◆ revert_slice()

void revert_slice ( symex_target_equationt & equation )

Undo whatever has been done by slice

Definition at line 261 of file slice.cpp.

◆ simple_slice()

void simple_slice ( symex_target_equationt & equation )

Definition at line 234 of file slice.cpp.

◆ slice() [1/2]

void slice ( symex_target_equationt & equation )

Definition at line 205 of file slice.cpp.

◆ 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: [out] equation symex trace to be sliced

expressions list of expressions, targets for slicing

Definition at line 226 of file slice.cpp.