14 #ifndef CPROVER_GOTO_INSTRUMENT_AGGRESSIVE_SLICER_H 15 #define CPROVER_GOTO_INSTRUMENT_AGGRESSIVE_SLICER_H 19 #include <unordered_set> 63 for(
const auto &f : function_list)
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)" 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...
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
bool preserve_all_direct_paths
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...
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)
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...
message_handlert & message_handler
std::list< std::string > user_specified_properties
Directed graph representation of this call graph.
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)