cprover
reachability_slicert Class Reference

#include <reachability_slicer_class.h>

Collaboration diagram for reachability_slicert:
[legend]

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_entrytcfgt
 
typedef std::stack< cfgt::entrytqueuet
 

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_indextget_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...
 

Detailed Description

Definition at line 22 of file reachability_slicer_class.h.

Member Typedef Documentation

◆ cfgt

Definition at line 49 of file reachability_slicer_class.h.

◆ queuet

Definition at line 52 of file reachability_slicer_class.h.

Member Function Documentation

◆ fixedpoint_from_assertions()

void reachability_slicert::fixedpoint_from_assertions ( const is_threadedt is_threaded,
slicing_criteriont criterion 
)
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.

Parameters
is_threadedInstructions that might be executed concurrently
criterionthe 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()().

◆ fixedpoint_to_assertions()

void reachability_slicert::fixedpoint_to_assertions ( const is_threadedt is_threaded,
slicing_criteriont criterion 
)
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.

Parameters
is_threadedInstructions that might be executed concurrently
criterionthe 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()().

◆ get_sources()

std::vector< reachability_slicert::cfgt::node_indext > reachability_slicert::get_sources ( const is_threadedt is_threaded,
slicing_criteriont criterion 
)
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.

Parameters
is_threadedInstructions that might be executed concurrently
criterionThe 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().

◆ operator()()

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

◆ slice()

void reachability_slicert::slice ( goto_functionst goto_functions)
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()().

Member Data Documentation

◆ cfg

cfgt reachability_slicert::cfg
protected

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