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[]);
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 completeassigns
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 clauseassigns \result \from ...;
:The
assigns
clause indicates thatsome_function
might change the value ofx
, and that the new value will be computed from the addresses stored inints[..]
(theindirect
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 intooutput.c
.) gives the following result:Note in addition that your example is not well-typed:
&p
is a pointer to pointer to int, and should thus be stored in anint**
array, not anint*
array. But I assume that it only stems from reducing your original example and is does not matter much for slicing itself.