20 const irep_idt &destination_function)
28 for(
const auto &func :
44 if(!fct.second.is_inlined())
46 for(
const auto &ins : fct.second.body.instructions)
62 if(
id2string(f_it->first).find(name_snippet) != std::string::npos)
79 message.
debug() <<
"No properties given, so aggressive slicer " 80 <<
"is running over all possible properties" 93 if(!property_loc.has_value())
94 throw "unable to find property in call graph";
107 message.
debug() <<
"Preserving the following functions \n";
const std::string & id2string(const irep_idt &d)
Remove function definition.
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_mapt function_map
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
#define INITIALIZE_FUNCTION
void remove_function(goto_modelt &goto_model, const irep_idt &identifier, message_handlert &message_handler)
Remove the body of function "identifier" such that an analysis will treat it as a side-effect free fu...
std::list< std::string > name_snippets
std::set< irep_idt > functions_to_keep
std::set< irep_idt > get_functions_reachable_within_n_steps(const call_grapht::directed_grapht &graph, const std::set< irep_idt > &start_functions, std::size_t n)
Get either callers or callees reachable from a given list of functions within N steps.
void doit()
Removes the body of all functions except those on the shortest path or functions that are reachable f...
Class that provides messages with a built-in verbosity 'level'.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
message_handlert & message_handler
std::set< irep_idt > get_reaching_functions(const call_grapht::directed_grapht &graph, const irep_idt &function)
Get functions that can reach a given function.
std::list< std::string > user_specified_properties
Aggressive slicer Consider the control flow graph of the goto program and a criterion description of ...
Function Call Graph Helpers.
#define forall_goto_functions(it, functions)
const irep_idt start_function
goto_functionst goto_functions
GOTO functions.
optionalt< source_locationt > find_property(const irep_idt &property, const goto_functionst &goto_functions)
Returns a source_locationt that corresponds to the property given by an irep_idt.
std::list< irep_idt > get_shortest_function_path(const call_grapht::directed_grapht &graph, const irep_idt &src, const irep_idt &dest)
Get list of functions on the shortest path between two functions.