2

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[]);
Justus Adam
  • 43
  • 5

1 Answers1

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.

Virgile
  • 9,724
  • 18
  • 42
  • Thank you that was a really good description. I tried it with the `assigns \result \from`, works like a charm. A refinement question: Say `some_function` neither modifies state, nor returns anything, but I need to preserve it for a side effect (failing assert). Is there a clean way to model this with `assigns`? PS: Yes the typing was accidental, it should have just been `{p}` – Justus Adam May 05 '20 at 12:54
  • No, I'm afraid it is not possible to model cleanly a function that might not terminate (from the caller point of view, an assert failure in the callee is a non-termination case in the sense that the remainder of the code never gets executed) with just `assigns`. – Virgile May 05 '20 at 14:25
  • 1
    Plus this kind of "effect" is very hard to keep through slicing, at least the one from Frama-C. – byako May 07 '20 at 08:55