cprover
|
#include <reachability_slicer_class.h>
Classes | |
struct | slicer_entryt |
Public Member Functions | |
void | operator() (goto_functionst &goto_functions, slicing_criteriont &criterion) |
Protected Types | |
typedef cfg_baset< slicer_entryt > | cfgt |
typedef std::stack< cfgt::entryt > | queuet |
Protected Member Functions | |
void | fixedpoint_assertions (const is_threadedt &is_threaded, slicing_criteriont &criterion) |
void | slice (goto_functionst &goto_functions) |
Protected Attributes | |
cfgt | cfg |
Definition at line 22 of file reachability_slicer_class.h.
|
protected |
Definition at line 45 of file reachability_slicer_class.h.
|
protected |
Definition at line 48 of file reachability_slicer_class.h.
|
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()().
|
inline |
Definition at line 25 of file reachability_slicer_class.h.
References cfg, fixedpoint_assertions(), and slice().
|
protected |
Definition at line 58 of file reachability_slicer.cpp.
References cfg, cfg_baset< T, P, I >::entry_map, Forall_goto_functions, Forall_goto_program_instructions, remove_skip(), remove_unreachable(), and goto_functions_templatet< bodyT >::update().
Referenced by operator()().
|
protected |
Definition at line 46 of file reachability_slicer_class.h.
Referenced by fixedpoint_assertions(), operator()(), and slice().