CODEWITHSUNDEEP
cframa-c
DaviD.
DaviD.

Reputation: 475

Frama-C: Getting function outputs when using pointers

I need to get a list of all the outputs of a function. When I use the From-plugin on the following code

void add(int *sum, int a, int b)
{
    *sum = a + b;
}

int main()
{
    int result;
    add(&result, 1, 2);
}

it tells me that result is the output of the add function. This is of course correct, but I would like the plugin to mention sum somewhere. I know sum is a pointer and is not modified in the function, so it is not an output, but *sum is modified and I would like to know that. Is there an easy (or any) way to achieve this?

Upvotes: 1

Views: 213

Answers (1)

Virgile
Virgile

Reputation: 10148

If you set add as your main entry point, you might be able to retrieve the information you want:

$ frama-c -main add -deps file.c
[...]
[from] ====== DEPENDENCIES COMPUTED ======
   These dependencies hold at termination for the executions that terminate:
[from] Function add:
  S_sum[0] FROM sum; a; b

Basically, S_sum[0] is *sum: Value (on which From relies) generates an initial state in which pointers are either NULL or pointing to a block with a name similar to the one of the pointer and having, by default, two elements. There are command line options to tweak the default behavior (see Value Analysis manual for more information on that), but you might find out that for more complex examples you need to write (or generate) a wrapper function that will set up a more complex initial state before calling the function. In that case, you'll have to keep track of which pointer points to where in order to reconstruct the information.

The bulk of the issue is that in the abstract state of Value, sum is mapped to a set L of possible locations (here reduced to a singleton), but *sum is not an object in itself. A write access will simply update all values mapped to elements of L. Thus from the point of view of From everything looks like a modification of result (or S_sum[0] if you change the entry point).

Upvotes: 2

Related Questions