reachability_slicer.h File Reference

#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   "(fp-reachability-slice):(reachability-slice)(reachability-slice-fb)"
#define	HELP_REACHABILITY_SLICER
#define	HELP_REACHABILITY_SLICER_FB

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_REACHABILITY_SLICER

#define HELP_REACHABILITY_SLICER

Value:

  " --fp-reachability-slice f    remove instructions that cannot appear on a trace\n" \
  "                              that visits all given functions. The list of\n"      \
  "                              functions has to be given as a comma separated\n"    \
  "                              list f.\n"                                           \
  " --reachability-slice         remove instructions that cannot appear on a trace\n" \
  "                              from entry point to a property\n"

Definition at line 48 of file reachability_slicer.h.

HELP_REACHABILITY_SLICER_FB

#define HELP_REACHABILITY_SLICER_FB

Value:

  " --reachability-slice-fb      remove instructions that cannot appear on a trace\n" \
  "                              from entry point through a property\n"

Definition at line 55 of file reachability_slicer.h.

OPT_REACHABILITY_SLICER

#define OPT_REACHABILITY_SLICER   "(fp-reachability-slice):(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.