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

static bool is_same_target (goto_programt::const_targett it1, goto_programt::const_targett it2)
 
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 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

◆ is_same_target()

◆ reachability_slicer() [1/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 217 of file reachability_slicer.cpp.

References goto_modelt::goto_functions.

Referenced by goto_instrument_parse_optionst::instrument_goto_program(), jbmc_parse_optionst::process_goto_functions(), cbmc_parse_optionst::process_goto_program(), and reachability_slicer().

◆ reachability_slicer() [2/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 233 of file reachability_slicer.cpp.

References goto_modelt::goto_functions.

◆ reachability_slicer() [3/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 247 of file reachability_slicer.cpp.

References reachability_slicer().

◆ reachability_slicer() [4/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 257 of file reachability_slicer.cpp.

References reachability_slicer().