cprover
|
#include <reachability_slicer_class.h>
Classes | |
struct | search_stack_entryt |
A search stack entry, used in tracking nodes to mark reachable when walking over the CFG in fixedpoint_to_assertions and fixedpoint_from_assertions . More... | |
struct | slicer_entryt |
Public Member Functions | |
void | operator() (goto_functionst &goto_functions, slicing_criteriont &criterion, bool include_forward_reachability) |
Protected Types | |
typedef cfg_baset< slicer_entryt > | cfgt |
typedef std::stack< cfgt::entryt > | queuet |
Protected Member Functions | |
void | fixedpoint_to_assertions (const is_threadedt &is_threaded, slicing_criteriont &criterion) |
Perform backwards depth-first search of the control-flow graph of the goto program, starting from the nodes corresponding to the criterion and the instructions that might be executed concurrently. More... | |
void | fixedpoint_from_assertions (const is_threadedt &is_threaded, slicing_criteriont &criterion) |
Perform forwards depth-first search of the control-flow graph of the goto program, starting from the nodes corresponding to the criterion and the instructions that might be executed concurrently. More... | |
void | slice (goto_functionst &goto_functions) |
This function removes all instructions that have the flag reaches_assertion or reachable_from_assertion set to true;. More... | |
Protected Attributes | |
cfgt | cfg |
Private Member Functions | |
std::vector< cfgt::node_indext > | get_sources (const is_threadedt &is_threaded, slicing_criteriont &criterion) |
Get the set of nodes that correspond to the given criterion, or that can appear in concurrent execution. More... | |
Definition at line 22 of file reachability_slicer_class.h.
|
protected |
Definition at line 49 of file reachability_slicer_class.h.
|
protected |
Definition at line 52 of file reachability_slicer_class.h.
|
protected |
Perform forwards depth-first search of the control-flow graph of the goto program, starting from the nodes corresponding to the criterion and the instructions that might be executed concurrently.
Set reaches_assertion to true for every instruction visited.
is_threaded | Instructions that might be executed concurrently |
criterion | the criterion we are trying to hit |
Definition at line 118 of file reachability_slicer.cpp.
References cfg, criterion, cfg_baset< T, P, I >::entry_map, get_sources(), INVARIANT, is_same_target(), grapht< N >::out(), and stack.
Referenced by operator()().
|
protected |
Perform backwards depth-first search of the control-flow graph of the goto program, starting from the nodes corresponding to the criterion and the instructions that might be executed concurrently.
Set reaches_assertion to true for every instruction visited.
is_threaded | Instructions that might be executed concurrently |
criterion | the criterion we are trying to hit |
Definition at line 62 of file reachability_slicer.cpp.
References cfg, criterion, cfg_baset< T, P, I >::entry_map, get_sources(), INVARIANT, is_same_target(), and stack.
Referenced by operator()().
|
private |
Get the set of nodes that correspond to the given criterion, or that can appear in concurrent execution.
None of these should be sliced away so they are used as a basis for the search.
is_threaded | Instructions that might be executed concurrently |
criterion | The criterion we care about |
Definition at line 33 of file reachability_slicer.cpp.
References cfg, criterion, and cfg_baset< T, P, I >::entry_map.
Referenced by fixedpoint_from_assertions(), and fixedpoint_to_assertions().
|
inline |
Definition at line 25 of file reachability_slicer_class.h.
References cfg, criterion, fixedpoint_from_assertions(), fixedpoint_to_assertions(), and slice().
|
protected |
This function removes all instructions that have the flag reaches_assertion or reachable_from_assertion set to true;.
Definition at line 186 of file reachability_slicer.cpp.
References cfg, cfg_baset< T, P, I >::entry_map, Forall_goto_functions, Forall_goto_program_instructions, remove_skip(), and remove_unreachable().
Referenced by operator()().
|
protected |
Definition at line 50 of file reachability_slicer_class.h.
Referenced by fixedpoint_from_assertions(), fixedpoint_to_assertions(), get_sources(), operator()(), and slice().