Slicer for symex traces. More...

#include "symex_target_equation.h"

Include dependency graph for slice.h:

This graph shows which files directly or indirectly include 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...

Detailed Description

Slicer for symex traces.

Definition in file slice.h.

Typedef Documentation

◆ symbol_sett

typedef std::unordered_set<irep_idt, irep_id_hash> symbol_sett

Definition at line 29 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
open_variables	target 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 239 of file slice.cpp.

References symex_target_equationt::SSA_steps.

Referenced by bmct::run().

◆ 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(), and bmct::run().

◆ slice() [2/2]

void slice	(	symex_target_equationt &	equation,
		const expr_listt &	expressions
	)

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