cprover
reachability_slicer.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Slicing
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
12#ifndef CPROVER_GOTO_INSTRUMENT_REACHABILITY_SLICER_H
13#define CPROVER_GOTO_INSTRUMENT_REACHABILITY_SLICER_H
14
15#include <list>
16#include <string>
17
18class goto_modelt;
19
21
24 const std::list<std::string> &properties);
25
27 goto_modelt &goto_model,
28 const std::list<std::string> &functions_list);
29
32 const bool include_forward_reachability);
33
36 const std::list<std::string> &properties,
37 const bool include_forward_reachability);
38
39// clang-format off
40#define OPT_REACHABILITY_SLICER \
41 "(fp-reachability-slice):(reachability-slice)(reachability-slice-fb)" // NOLINT(*)
42
43#define HELP_REACHABILITY_SLICER \
44 " --fp-reachability-slice f remove instructions that cannot appear on a trace\n" \
45 " that visits all given functions. The list of\n" \
46 " functions has to be given as a comma separated\n" \
47 " list f.\n" \
48 " --reachability-slice remove instructions that cannot appear on a trace\n" \
49 " from entry point to a property\n" // NOLINT(*)
50#define HELP_REACHABILITY_SLICER_FB \
51 " --reachability-slice-fb remove instructions that cannot appear on a trace\n" \
52 " from entry point through a property\n" // NOLINT(*)
53// clang-format on
54#endif // CPROVER_GOTO_INSTRUMENT_REACHABILITY_SLICER_H
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.
void reachability_slicer(goto_modelt &)
Perform reachability slicing on goto_model, with respect to criterion comprising all properties.