cprover
reachability_slicer.cpp File Reference

Reachability Slicer Consider the control flow graph of the goto program and a criterion, and remove the parts of the graph from which the criterion is not reachable (and possibly, depending on the parameters, keep those that can be reached from the criterion). More...

+ Include dependency graph for reachability_slicer.cpp:

Go to the source code of this file.

Functions

void reachability_slicer (goto_modelt &goto_model, const bool include_forward_reachability)
 Perform reachability slicing on goto_model, with respect to the criterion given by all properties. More...
 
void reachability_slicer (goto_modelt &goto_model, const std::list< std::string > &properties, const bool include_forward_reachability)
 Perform reachability slicing on goto_model for selected properties. More...
 
void function_path_reachability_slicer (goto_modelt &goto_model, const std::list< std::string > &functions_list)
 Perform reachability slicing on goto_model for selected functions. More...
 
void reachability_slicer (goto_modelt &goto_model)
 Perform reachability slicing on goto_model, with respect to criterion comprising all properties. More...
 
void reachability_slicer (goto_modelt &goto_model, const std::list< std::string > &properties)
 Perform reachability slicing on goto_model for selected properties. More...
 

Detailed Description

Reachability Slicer Consider the control flow graph of the goto program and a criterion, and remove the parts of the graph from which the criterion is not reachable (and possibly, depending on the parameters, keep those that can be reached from the criterion).

Definition in file reachability_slicer.cpp.

Function Documentation

◆ function_path_reachability_slicer()

void function_path_reachability_slicer ( goto_modelt goto_model,
const std::list< std::string > &  functions_list 
)

Perform reachability slicing on goto_model for selected functions.

Parameters
goto_modelGoto program to slice
functions_listThe functions relevant for the slicing (i.e. starting point for the search in the CFG). Anything that is reachable in the CFG starting from these functions will be kept.

Definition at line 399 of file reachability_slicer.cpp.

◆ reachability_slicer() [1/4]

void reachability_slicer ( goto_modelt goto_model)

Perform reachability slicing on goto_model, with respect to criterion comprising all properties.

Only instructions from which the criterion is reachable will be kept.

Parameters
goto_modelGoto program to slice

Definition at line 421 of file reachability_slicer.cpp.

◆ reachability_slicer() [2/4]

void reachability_slicer ( goto_modelt goto_model,
const bool  include_forward_reachability 
)

Perform reachability slicing on goto_model, with respect to the criterion given by all properties.

Parameters
goto_modelGoto program to slice
include_forward_reachabilityDetermines if only instructions from which the criterion is reachable should be kept (false) or also those reachable from the criterion (true)

Definition at line 368 of file reachability_slicer.cpp.

◆ reachability_slicer() [3/4]

void reachability_slicer ( goto_modelt goto_model,
const std::list< std::string > &  properties 
)

Perform reachability slicing on goto_model for selected properties.

Only instructions from which the criterion is reachable will be kept.

Parameters
goto_modelGoto program to slice
propertiesThe properties relevant for the slicing (i.e. starting point for the search in the cfg)

Definition at line 431 of file reachability_slicer.cpp.

◆ reachability_slicer() [4/4]

void reachability_slicer ( goto_modelt goto_model,
const std::list< std::string > &  properties,
const bool  include_forward_reachability 
)

Perform reachability slicing on goto_model for selected properties.

Parameters
goto_modelGoto program to slice
propertiesThe properties relevant for the slicing (i.e. starting point for the search in the cfg)
include_forward_reachabilityDetermines if only instructions from which the criterion is reachable should be kept (false) or also those reachable from the criterion (true)

Definition at line 384 of file reachability_slicer.cpp.