cprover
aggressive_slicer.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Aggressive Slicer
4 
5 Author: Elizabeth Polgreen, polgreen@amazon.com
6 
7 \*******************************************************************/
8 
13 
14 #ifndef CPROVER_GOTO_INSTRUMENT_AGGRESSIVE_SLICER_H
15 #define CPROVER_GOTO_INSTRUMENT_AGGRESSIVE_SLICER_H
16 
17 #include <list>
18 #include <string>
19 #include <unordered_set>
20 
21 #include <util/irep.h>
22 
23 #include <analyses/call_graph.h>
24 
26 
27 class goto_modelt;
28 class message_handlert;
29 
37 {
38 public:
40  : call_depth(0),
42  start_function(_goto_model.goto_functions.entry_point()),
43  goto_model(_goto_model),
44  message_handler(_msg)
45  {
46  call_grapht undirected_call_graph =
48  call_graph = undirected_call_graph.get_directed_graph();
49  }
50 
55  void doit();
56 
61  void preserve_functions(const std::list<std::string> &function_list)
62  {
63  for(const auto &f : function_list)
64  functions_to_keep.insert(f);
65  };
66 
67  std::list<std::string> user_specified_properties;
68  std::size_t call_depth;
69  std::list<std::string> name_snippets;
71 
72 private:
76  std::set<irep_idt> functions_to_keep;
78 
83 
90  void note_functions_to_keep(const irep_idt &destination_function);
91 
98 };
99 
100 // clang-format off
101 #define OPT_AGGRESSIVE_SLICER \
102  "(aggressive-slice)" \
103  "(aggressive-slice-call-depth):" \
104  "(aggressive-slice-preserve-function):" \
105  "(aggressive-slice-preserve-functions-containing):" \
106  "(aggressive-slice-preserve-all-direct-paths)"
107 
108 // clang-format on
109 
110 #endif // CPROVER_GOTO_INSTRUMENT_AGGRESSIVE_SLICER_H
void find_functions_that_contain_name_snippet()
Finds all functions whose name contains a name snippet and adds them to the std::unordered_set of ire...
Function Call Graphs.
void note_functions_to_keep(const irep_idt &destination_function)
notes functions to keep in the slice based on the program start function and the given destination fu...
void get_all_functions_containing_properties()
Finds all functions that contain a property, and adds them to the list of functions to keep...
call_grapht::directed_grapht call_graph
void preserve_functions(const std::list< std::string > &function_list)
Adds a list of functions to the set of functions for the aggressive slicer to preserve.
directed_grapht get_directed_graph() const
Returns a grapht representation of this call graph, suitable for use with generic grapht algorithms...
Definition: call_graph.cpp:208
std::list< std::string > name_snippets
std::set< irep_idt > functions_to_keep
static call_grapht create_from_root_function(const goto_modelt &model, const irep_idt &root, bool collect_callsites)
Definition: call_graph.h:31
void doit()
Removes the body of all functions except those on the shortest path or functions that are reachable f...
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
message_handlert & message_handler
goto_modelt & goto_model
std::list< std::string > user_specified_properties
Directed graph representation of this call graph.
Definition: call_graph.h:117
The aggressive slicer removes the body of all the functions except those on the shortest path...
const irep_idt start_function
aggressive_slicert(goto_modelt &_goto_model, message_handlert &_msg)