CBMC
aggressive_slicert Class Reference

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>

+ Collaboration diagram for aggressive_slicert:

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_modeltgoto_model
 
message_handlertmessage_handler
 
std::set< irep_idtfunctions_to_keep
 
call_grapht::directed_grapht call_graph
 

Detailed Description

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 34 of file aggressive_slicer.h.

Constructor & Destructor Documentation

◆ aggressive_slicert()

aggressive_slicert::aggressive_slicert ( goto_modelt _goto_model,
message_handlert _msg 
)
inline

Definition at line 37 of file aggressive_slicer.h.

Member Function Documentation

◆ doit()

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 76 of file aggressive_slicer.cpp.

◆ find_functions_that_contain_name_snippet()

void aggressive_slicert::find_functions_that_contain_name_snippet ( )
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 64 of file aggressive_slicer.cpp.

◆ get_all_functions_containing_properties()

void aggressive_slicert::get_all_functions_containing_properties ( )
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 46 of file aggressive_slicer.cpp.

◆ note_functions_to_keep()

void aggressive_slicert::note_functions_to_keep ( const irep_idt destination_function)
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

Parameters
destination_functionname 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 25 of file aggressive_slicer.cpp.

◆ preserve_functions()

void aggressive_slicert::preserve_functions ( const std::list< std::string > &  function_list)
inline

Adds a list of functions to the set of functions for the aggressive slicer to preserve.

Parameters
function_lista list of functions in form std::list<std::string>, as returned by get_cmdline_option.

Definition at line 59 of file aggressive_slicer.h.

Member Data Documentation

◆ call_depth

std::size_t aggressive_slicert::call_depth

Definition at line 66 of file aggressive_slicer.h.

◆ call_graph

call_grapht::directed_grapht aggressive_slicert::call_graph
private

Definition at line 75 of file aggressive_slicer.h.

◆ functions_to_keep

std::set<irep_idt> aggressive_slicert::functions_to_keep
private

Definition at line 74 of file aggressive_slicer.h.

◆ goto_model

goto_modelt& aggressive_slicert::goto_model
private

Definition at line 72 of file aggressive_slicer.h.

◆ message_handler

message_handlert& aggressive_slicert::message_handler
private

Definition at line 73 of file aggressive_slicer.h.

◆ name_snippets

std::list<std::string> aggressive_slicert::name_snippets

Definition at line 67 of file aggressive_slicer.h.

◆ preserve_all_direct_paths

bool aggressive_slicert::preserve_all_direct_paths

Definition at line 68 of file aggressive_slicer.h.

◆ start_function

const irep_idt aggressive_slicert::start_function
private

Definition at line 71 of file aggressive_slicer.h.

◆ user_specified_properties

std::list<std::string> aggressive_slicert::user_specified_properties

Definition at line 65 of file aggressive_slicer.h.


The documentation for this class was generated from the following files: