reachability_slicer.cpp File Reference

Reachability Slicer Consider the control flow graph of the goto program and a criterion, and remove the parts of the graph from which the criterion is not reachable (and possibly, depending on the parameters, keep those that can be reached from the criterion). More...

#include "full_slicer_class.h"
#include "reachability_slicer_class.h"
#include <util/exception_utils.h>
#include <goto-programs/cfg.h>
#include <goto-programs/remove_calls_no_body.h>
#include <goto-programs/remove_skip.h>
#include <goto-programs/remove_unreachable.h>
#include <analyses/is_threaded.h>
#include "reachability_slicer.h"

Include dependency graph for reachability_slicer.cpp:

Go to the source code of this file.

Functions
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. More...
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. More...
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. More...
void	reachability_slicer (goto_modelt &goto_model, message_handlert &message_handler)
	Perform reachability slicing on goto_model, with respect to criterion comprising all properties. More...
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. More...

Detailed Description

Reachability Slicer Consider the control flow graph of the goto program and a criterion, and remove the parts of the graph from which the criterion is not reachable (and possibly, depending on the parameters, keep those that can be reached from the criterion).

Definition in file reachability_slicer.cpp.

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.