frama-c slicing plugin appears to discard used stack values

Question

Problem description

I'm developing a frama-c plugin that uses the slicing plugin as a library to remove unused bits of automatically generated code. Unfortunately the slicing plugin drops a bunch of stack values, which are actually used. They are used in so far as their addresses are contained in structures that are handed of to abstract external functions.

Simple example

This is a simpler example that models the same general structure I have.

/* Abstract external function */
void some_function(int* ints[]);

int main() {
  int i;
  int *p = &i;
  int *a[] = { &p };
  some_function(a);
  return 0;
}

When slicing this example with frama-c-gui -slice-calls some_function experiment_slicing.c (I haven't figures out how to see the slicing output when invoking the command line without gui) it drops everything but the declaration int *a[]; and the call to some_function.

Attempted fixes

I tried fixing it by adding ACSL annotations. However what I believed to be the sensible specification (see below) did not work

/*@ requires \valid(ints) && \valid(ints[0]);
 */
void some_function(int* ints[]);

I then tried with an assign (see below) which does have the desired behaviour. however it is not a correct specification, since the function never actually writes to the pointer but needs to read it for correct functionality. I am worried that if I move ahead with such an incorrect specification it will lead to weird problems down the line.

/*@ requires \valid(ints) && \valid(ints[0]);
   assigns  *ints;
*/
void some_function(int* ints[]);

Answer 1

You are on the right track: it is the assigns clause that you should use here: it will indicate which parts of the memory state are concerned by a call to an undefined function. However, you need to provide a complete assigns clause, with its \from part (that indicates which memory location are read to compute the new value of the memory location written to).

I have added an int variable to your example, as your function isn't returning a result (void return type). For a function that is returning something, you should also have a clause assigns \result \from ...;:

int x;

/*@ assigns x \from indirect:ints[..], *(ints[..]); */
void some_function(int* ints[]);

int main() {
  int i;
  int*p = &i;
  int *a[] = { &p };
  some_function(a);
  return 0;
}

The assigns clause indicates that some_function might change the value of x, and that the new value will be computed from the addresses stored in ints[..] (the indirect label tells that we're not using their value directly, this is described in more detail in section 8.2 of Eva's manual), and their content.

using frama-c -slice-calls some_function file.c -then-last -print (the last arguments are here to print the resulting file on the standard output: -then-last indicates that the following options should operate on the last Frama-C project created, in that case the one resulting from the slicing, and -print prints the C code of said project. You may also use -ocode output.c to redirect the pretty-printing of the code into output.c.) gives the following result:

* Generated by Frama-C */
void some_function(int **ints);

void main(void)
{
  int i;
  int *p = & i;
  int *a[1] = {(int *)(& p)};
  some_function(a);
  return;
}

Note in addition that your example is not well-typed: &p is a pointer to pointer to int, and should thus be stored in an int** array, not an int* array. But I assume that it only stems from reducing your original example and is does not matter much for slicing itself.