cprover
reachability_slicer.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Slicing
4 
5 Author: 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 
18 class goto_modelt;
19 
21 
23  goto_modelt &,
24  const std::list<std::string> &properties);
25 
27  goto_modelt &goto_model,
28  const std::list<std::string> &functions_list);
29 
31  goto_modelt &,
32  const bool include_forward_reachability);
33 
35  goto_modelt &,
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
function_path_reachability_slicer
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.
Definition: reachability_slicer.cpp:399
goto_modelt
Definition: goto_model.h:26
reachability_slicer
void reachability_slicer(goto_modelt &)
Perform reachability slicing on goto_model, with respect to criterion comprising all properties.
Definition: reachability_slicer.cpp:421