cprover
|
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 "reachability_slicer.h"
#include <stack>
#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 <util/exception_utils.h>
#include <util/message.h>
#include "full_slicer_class.h"
#include "reachability_slicer_class.h"
Go to the source code of this file.
Functions | |
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. More... | |
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. More... | |
void | function_path_reachability_slicer (goto_modelt &goto_model, const std::list< std::string > &functions_list) |
Perform reachability slicing on goto_model for selected functions. More... | |
void | reachability_slicer (goto_modelt &goto_model) |
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) |
Perform reachability slicing on goto_model for selected properties. More... | |
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.
void function_path_reachability_slicer | ( | goto_modelt & | goto_model, |
const std::list< std::string > & | functions_list | ||
) |
Perform reachability slicing on goto_model for selected functions.
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. |
Definition at line 399 of file reachability_slicer.cpp.
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 421 of file reachability_slicer.cpp.
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 368 of file reachability_slicer.cpp.
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 431 of file reachability_slicer.cpp.
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 384 of file reachability_slicer.cpp.