symex_slicet Class Reference

#include <symex_slice_class.h>

Collaboration diagram for symex_slicet:

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

Protected Member Functions
void	get_symbols (const exprt &expr)
void	slice (SSA_stept &SSA_step)
void	slice_assignment (SSA_stept &SSA_step)
void	slice_decl (SSA_stept &SSA_step)

Protected Attributes
symbol_sett	depends

Detailed Description

Definition at line 18 of file symex_slice_class.h.

Member Function Documentation

collect_open_variables()

void symex_slicet::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 138 of file slice.cpp.

get_symbols()

void symex_slicet::get_symbols ( const exprt &  expr )

protected

Definition at line 18 of file slice.cpp.

slice() [1/3]

void symex_slicet::slice ( SSA_stept &  SSA_step )

protected

Definition at line 48 of file slice.cpp.

slice() [2/3]

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

Definition at line 23 of file slice.cpp.

slice() [3/3]

void symex_slicet::slice

(

symex_target_equationt &

equation

)

Definition at line 34 of file slice.cpp.

slice_assignment()

void symex_slicet::slice_assignment ( SSA_stept &  SSA_step )

protected

Definition at line 104 of file slice.cpp.

slice_decl()

void symex_slicet::slice_decl ( SSA_stept &  SSA_step )

protected

Definition at line 123 of file slice.cpp.

Member Data Documentation

depends

symbol_sett symex_slicet::depends

protected

Definition at line 30 of file symex_slice_class.h.

---

The documentation for this class was generated from the following files:

• /home/runner/work/cbmc/cbmc/src/goto-symex/symex_slice_class.h
• /home/runner/work/cbmc/cbmc/src/goto-symex/slice.cpp