slice.cpp File Reference

#include "slice.h"
#include "symex_slice_class.h"
#include <util/find_symbols.h>
#include <util/std_expr.h>

Include dependency graph for slice.cpp:

Go to the source code of this file.

Functions
void	slice (symex_target_equationt &equation)
void	collect_open_variables (const symex_target_equationt &equation, symbol_sett &open_variables)
	Collect the open variables, i.e. More...
void	slice (symex_target_equationt &equation, const std::list< exprt > &expressions)
	Slice the symex trace with respect to a list of expressions. More...
void	simple_slice (symex_target_equationt &equation)
void	revert_slice (symex_target_equationt &equation)
	Undo whatever has been done by slice More...

Detailed Description

Slicer for symex traces

Definition in file slice.cpp.

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.