[SOLVED] Slicing using frama-c

Slicing using frama-c

I'm using frama-c in order to do some experiments on program slicing. The tool is great and there are a lot of different types of slicing (by result or by statement, for example). I'm using a program data structure like:

typedef struct ComplexData {
    int x;
    int y;
    char string_[100];
    size_t n;
} ComplexData;

It's just an example in order to understand how frama-c can slice the program by the result produced by the function. Basically, the main method calls a function which returns a value of the type ComplexData. How the comparison between different executions is performed? There is a check for each value of the struct? Like this?

Solution

The option -slice-return f of Frama-C instructs the slicer to keep all statements that contribute to the computation of the return code of f. For your type ComplexData, this means the contents of any of the fields. Any statement that computes e.g. y, or one the characters in string_, will be kept.

Regarding comparison between different executions, static slicers actually work differently. They approximate the behavior of each function, across all possible executions. (In the case of Frama-C, this is done using a technique known as abstract interpretation.) Thus, there is no need to compare two executions.