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
static mstreamt & eom(mstreamt &m)
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...
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.