cprover
|
The aggressive slicer removes the body of all the functions except those on the shortest path, those within the call-depth of the shortest path, those given by name as command line argument, and those that contain a given irep_idt snippet If no properties are set by the user, we preserve all functions on the shortest paths to each property. More...
#include <aggressive_slicer.h>
Public Member Functions | |
aggressive_slicert (goto_modelt &_goto_model, message_handlert &_msg) | |
void | doit () |
Removes the body of all functions except those on the shortest path or functions that are reachable from functions on the shortest path within N calls, where N is given by the parameter "distance". More... | |
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. More... | |
Public Attributes | |
std::list< std::string > | user_specified_properties |
std::size_t | call_depth |
std::list< std::string > | name_snippets |
bool | preserve_all_direct_paths |
Private Member Functions | |
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 irep_idts of functions for the aggressive slicer to preserve. More... | |
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 function. More... | |
void | get_all_functions_containing_properties () |
Finds all functions that contain a property, and adds them to the list of functions to keep. More... | |
Private Attributes | |
const irep_idt | start_function |
goto_modelt & | goto_model |
message_handlert & | message_handler |
std::set< irep_idt > | functions_to_keep |
call_grapht::directed_grapht | call_graph |
The aggressive slicer removes the body of all the functions except those on the shortest path, those within the call-depth of the shortest path, those given by name as command line argument, and those that contain a given irep_idt snippet If no properties are set by the user, we preserve all functions on the shortest paths to each property.
Definition at line 36 of file aggressive_slicer.h.
|
inline |
Definition at line 39 of file aggressive_slicer.h.
References call_graph, call_grapht::create_from_root_function(), call_grapht::get_directed_graph(), goto_model, and start_function.
void aggressive_slicert::doit | ( | ) |
Removes the body of all functions except those on the shortest path or functions that are reachable from functions on the shortest path within N calls, where N is given by the parameter "distance".
Definition at line 68 of file aggressive_slicer.cpp.
References call_depth, call_graph, messaget::debug(), messaget::eom(), find_functions_that_contain_name_snippet(), find_property(), forall_goto_functions, functions_to_keep, get_all_functions_containing_properties(), get_functions_reachable_within_n_steps(), goto_modelt::goto_functions, goto_model, INITIALIZE_FUNCTION, message_handler, name_snippets, note_functions_to_keep(), remove_function(), start_function, and user_specified_properties.
Referenced by goto_instrument_parse_optionst::instrument_goto_program().
|
private |
Finds all functions whose name contains a name snippet and adds them to the std::unordered_set of irep_idts of functions for the aggressive slicer to preserve.
Definition at line 56 of file aggressive_slicer.cpp.
References forall_goto_functions, functions_to_keep, goto_modelt::goto_functions, goto_model, id2string(), and name_snippets.
Referenced by doit().
|
private |
Finds all functions that contain a property, and adds them to the list of functions to keep.
This function is only called if no properties are given by the user. This behaviour mirrors the behaviour of the other program slicers (reachability, global, full)
Definition at line 40 of file aggressive_slicer.cpp.
References goto_functionst::function_map, functions_to_keep, goto_modelt::goto_functions, goto_model, and note_functions_to_keep().
Referenced by doit().
|
private |
notes functions to keep in the slice based on the program start function and the given destination function.
Functions are noted according to the configuration parameters set in the aggressive slicer, i.e., shortest path between two functions, or all direct paths. Inserts functions to preserve into the functions_to_keep set
destination_function | name of destination function for slice |
Note that we have previously disconnected all nodes unreachable from the start function, which means that any reaching functions are also reachable from the start function.
Definition at line 19 of file aggressive_slicer.cpp.
References call_graph, functions_to_keep, get_reaching_functions(), get_shortest_function_path(), preserve_all_direct_paths, and start_function.
Referenced by doit(), and get_all_functions_containing_properties().
|
inline |
Adds a list of functions to the set of functions for the aggressive slicer to preserve.
function_list | a list of functions in form std::list<std::string>, as returned by get_cmdline_option. |
Definition at line 61 of file aggressive_slicer.h.
References functions_to_keep.
Referenced by goto_instrument_parse_optionst::instrument_goto_program().
std::size_t aggressive_slicert::call_depth |
Definition at line 68 of file aggressive_slicer.h.
Referenced by doit(), and goto_instrument_parse_optionst::instrument_goto_program().
|
private |
Definition at line 77 of file aggressive_slicer.h.
Referenced by aggressive_slicert(), doit(), and note_functions_to_keep().
|
private |
Definition at line 76 of file aggressive_slicer.h.
Referenced by doit(), find_functions_that_contain_name_snippet(), get_all_functions_containing_properties(), note_functions_to_keep(), and preserve_functions().
|
private |
Definition at line 74 of file aggressive_slicer.h.
Referenced by aggressive_slicert(), doit(), find_functions_that_contain_name_snippet(), and get_all_functions_containing_properties().
|
private |
Definition at line 75 of file aggressive_slicer.h.
Referenced by doit().
std::list<std::string> aggressive_slicert::name_snippets |
Definition at line 69 of file aggressive_slicer.h.
Referenced by doit(), find_functions_that_contain_name_snippet(), and goto_instrument_parse_optionst::instrument_goto_program().
bool aggressive_slicert::preserve_all_direct_paths |
Definition at line 70 of file aggressive_slicer.h.
Referenced by goto_instrument_parse_optionst::instrument_goto_program(), and note_functions_to_keep().
|
private |
Definition at line 73 of file aggressive_slicer.h.
Referenced by aggressive_slicert(), doit(), and note_functions_to_keep().
std::list<std::string> aggressive_slicert::user_specified_properties |
Definition at line 65 of file aggressive_slicer.h.
Referenced by doit(), and goto_instrument_parse_optionst::instrument_goto_program().