cprover
Loading...
Searching...
No Matches
aggressive_slicer.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Aggressive Slicer
4
5Author: 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
20#include <util/irep.h>
21
22#include <analyses/call_graph.h>
23
25
27
35{
36public:
38 : call_depth(0),
40 start_function(_goto_model.goto_functions.entry_point()),
41 goto_model(_goto_model),
42 message_handler(_msg)
43 {
44 call_grapht undirected_call_graph =
46 call_graph = undirected_call_graph.get_directed_graph();
47 }
48
53 void doit();
54
59 void preserve_functions(const std::list<std::string> &function_list)
60 {
61 for(const auto &f : function_list)
62 functions_to_keep.insert(f);
63 };
64
65 std::list<std::string> user_specified_properties;
66 std::size_t call_depth;
67 std::list<std::string> name_snippets;
69
70private:
74 std::set<irep_idt> functions_to_keep;
76
81
88 void note_functions_to_keep(const irep_idt &destination_function);
89
96};
97
98// clang-format off
99#define OPT_AGGRESSIVE_SLICER \
100 "(aggressive-slice)" \
101 "(aggressive-slice-call-depth):" \
102 "(aggressive-slice-preserve-function):" \
103 "(aggressive-slice-preserve-functions-containing):" \
104 "(aggressive-slice-preserve-all-direct-paths)"
105
106// clang-format on
107
108#endif // CPROVER_GOTO_INSTRUMENT_AGGRESSIVE_SLICER_H
Function Call Graphs.
goto_modelt & goto_model
message_handlert & message_handler
std::list< std::string > user_specified_properties
call_grapht::directed_grapht call_graph
void doit()
Removes the body of all functions except those on the shortest path or functions that are reachable f...
std::list< std::string > name_snippets
aggressive_slicert(goto_modelt &_goto_model, message_handlert &_msg)
void get_all_functions_containing_properties()
Finds all functions that contain a property, and adds them to the list of functions to keep.
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.
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...
const irep_idt start_function
std::set< irep_idt > functions_to_keep
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...
Directed graph representation of this call graph.
Definition call_graph.h:140
A call graph (https://en.wikipedia.org/wiki/Call_graph) for a GOTO model or GOTO functions collection...
Definition call_graph.h:44
directed_grapht get_directed_graph() const
Returns a grapht representation of this call graph, suitable for use with generic grapht algorithms.
static call_grapht create_from_root_function(const goto_modelt &model, const irep_idt &root, bool collect_callsites)
Definition call_graph.h:53
Symbol Table + CFG.
dstringt irep_idt