CBMC
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_FP_REACHABILITY_SLICER   "(fp-reachability-slice):"
 
#define OPT_REACHABILITY_SLICER   "(reachability-slice)(reachability-slice-fb)"
 
#define HELP_FP_REACHABILITY_SLICER
 
#define HELP_REACHABILITY_SLICER
 

Functions

void reachability_slicer (goto_modelt &, message_handlert &)
 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, message_handlert &)
 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, message_handlert &)
 Perform reachability slicing on goto_model for selected functions. More...
 
void reachability_slicer (goto_modelt &, const bool include_forward_reachability, message_handlert &)
 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, message_handlert &)
 Perform reachability slicing on goto_model for selected properties. More...
 

Detailed Description

Slicing.

Definition in file reachability_slicer.h.

Macro Definition Documentation

◆ HELP_FP_REACHABILITY_SLICER

#define HELP_FP_REACHABILITY_SLICER
Value:
" {y--fp-reachability-slice} {uf} \t " \
"remove instructions that cannot appear on a trace that visits all given " \
"functions. The list of functions has to be given as a comma separated " \
"list {uf}.\n" \
" {y--reachability-slice} \t " \
"remove instructions that cannot appear on a trace from entry point to a " \
"property\n"

Definition at line 47 of file reachability_slicer.h.

◆ HELP_REACHABILITY_SLICER

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

Definition at line 55 of file reachability_slicer.h.

◆ OPT_FP_REACHABILITY_SLICER

#define OPT_FP_REACHABILITY_SLICER   "(fp-reachability-slice):"

Definition at line 44 of file reachability_slicer.h.

◆ OPT_REACHABILITY_SLICER

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

Definition at line 45 of file reachability_slicer.h.

Function Documentation

◆ function_path_reachability_slicer()

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

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.
message_handlermessage handler

Definition at line 438 of file reachability_slicer.cpp.

◆ reachability_slicer() [1/4]

void reachability_slicer ( goto_modelt goto_model,
const bool  include_forward_reachability,
message_handlert message_handler 
)

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)
message_handlermessage handler

Definition at line 397 of file reachability_slicer.cpp.

◆ reachability_slicer() [2/4]

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

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)
message_handlermessage handler

Definition at line 418 of file reachability_slicer.cpp.

◆ reachability_slicer() [3/4]

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

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)
message_handlermessage handler

Definition at line 476 of file reachability_slicer.cpp.

◆ reachability_slicer() [4/4]

void reachability_slicer ( goto_modelt goto_model,
message_handlert message_handler 
)

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
message_handlermessage handler

Definition at line 463 of file reachability_slicer.cpp.