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/remove_skip.h>
#include <goto-programs/remove_unreachable.h>
#include <goto-programs/cfg.h>
#include "full_slicer_class.h"
#include "reachability_slicer_class.h"
Go to the source code of this file.
Functions | |
static bool | is_same_target (goto_programt::const_targett it1, goto_programt::const_targett it2) |
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 | 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.
|
static |
Definition at line 47 of file reachability_slicer.cpp.
Referenced by reachability_slicert::fixedpoint_from_assertions(), and reachability_slicert::fixedpoint_to_assertions().
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 217 of file reachability_slicer.cpp.
References goto_modelt::goto_functions.
Referenced by goto_instrument_parse_optionst::instrument_goto_program(), jbmc_parse_optionst::process_goto_functions(), cbmc_parse_optionst::process_goto_program(), and reachability_slicer().
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 233 of file reachability_slicer.cpp.
References goto_modelt::goto_functions.
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 247 of file reachability_slicer.cpp.
References reachability_slicer().
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 257 of file reachability_slicer.cpp.
References reachability_slicer().