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_model	Goto program to slice
functions_list	The 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_handler	message 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_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)
message_handler	message 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_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)
message_handler	message 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_model	Goto program to slice
properties	The properties relevant for the slicing (i.e. starting point for the search in the cfg)
message_handler	message 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_model	Goto program to slice
message_handler	message handler

Definition at line 463 of file reachability_slicer.cpp.