cprover
|
Slicing. More...
#include <list>
#include <string>
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... | |
Slicing.
Definition in file reachability_slicer.h.
#define HELP_REACHABILITY_SLICER |
Definition at line 38 of file reachability_slicer.h.
Referenced by cbmc_parse_optionst::help(), and jbmc_parse_optionst::help().
Definition at line 35 of file reachability_slicer.h.
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.
goto_model | Goto program to slice |
Definition at line 247 of file reachability_slicer.cpp.
References reachability_slicer().
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.
goto_model | Goto program to slice |
properties | The 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().
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.
goto_model | Goto program to slice |
include_forward_reachability | Determines 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().
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.
goto_model | Goto program to slice |
properties | The properties relevant for the slicing (i.e. starting point for the search in the cfg) |
include_forward_reachability | Determines 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.