cprover
reachability_slicert Class Reference

#include <reachability_slicer_class.h>

Collaboration diagram for reachability_slicert:
[legend]

Classes

struct  slicer_entryt
 

Public Member Functions

void operator() (goto_functionst &goto_functions, slicing_criteriont &criterion)
 

Protected Types

typedef cfg_baset< slicer_entrytcfgt
 
typedef std::stack< cfgt::entrytqueuet
 

Protected Member Functions

void fixedpoint_assertions (const is_threadedt &is_threaded, slicing_criteriont &criterion)
 
void slice (goto_functionst &goto_functions)
 

Protected Attributes

cfgt cfg
 

Detailed Description

Definition at line 22 of file reachability_slicer_class.h.

Member Typedef Documentation

◆ cfgt

Definition at line 45 of file reachability_slicer_class.h.

◆ queuet

Definition at line 48 of file reachability_slicer_class.h.

Member Function Documentation

◆ fixedpoint_assertions()

void reachability_slicert::fixedpoint_assertions ( const is_threadedt is_threaded,
slicing_criteriont criterion 
)
protected

Definition at line 23 of file reachability_slicer.cpp.

References cfg, cfg_baset< T, P, I >::entry_map, and graph_nodet< E >::in.

Referenced by operator()().

◆ operator()()

void reachability_slicert::operator() ( goto_functionst goto_functions,
slicing_criteriont criterion 
)
inline

Definition at line 25 of file reachability_slicer_class.h.

References cfg, fixedpoint_assertions(), and slice().

◆ slice()

Member Data Documentation

◆ cfg

cfgt reachability_slicert::cfg
protected

Definition at line 46 of file reachability_slicer_class.h.

Referenced by fixedpoint_assertions(), operator()(), and slice().


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