cprover
reachability_slicer.h File Reference

Slicing. More...

#include <list>
#include <string>
Include dependency graph for reachability_slicer.h:
This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Macros

#define OPT_REACHABILITY_SLICER   "(reachability-slice)(reachability-slice-fb)"
 
#define HELP_REACHABILITY_SLICER
 

Functions

void reachability_slicer (goto_modelt &)
 Perform reachability slicing on goto_model, with respect to criterion comprising all properties. More...
 
void reachability_slicer (goto_modelt &, const std::list< std::string > &properties)
 Perform reachability slicing on goto_model for selected properties. More...
 
void reachability_slicer (goto_modelt &, 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 &, const std::list< std::string > &properties, const bool include_forward_reachability)
 Perform reachability slicing on goto_model for selected properties. More...
 

Detailed Description

Slicing.

Definition in file reachability_slicer.h.

Macro Definition Documentation

◆ HELP_REACHABILITY_SLICER

#define HELP_REACHABILITY_SLICER
Value:
" --reachability-slice remove instructions that cannot appear on a " \
"trace from entry point to a property\n" \
" --reachability-slice-fb remove instructions that cannot appear on a " \
"trace from entry point through a property\n"

Definition at line 38 of file reachability_slicer.h.

Referenced by cbmc_parse_optionst::help(), and jbmc_parse_optionst::help().

◆ OPT_REACHABILITY_SLICER

#define OPT_REACHABILITY_SLICER   "(reachability-slice)(reachability-slice-fb)"

Definition at line 35 of file reachability_slicer.h.

Function Documentation

◆ 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 247 of file reachability_slicer.cpp.

References reachability_slicer().

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

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

References goto_modelt::goto_functions.