[SOLVED] Resolve array dependencies

Resolve array dependencies

I am currently working with Frama-C and the from plugin to get the dependencies between variables. If several elements of an array have the same dependency, this is output as a summary as follows: array[0..N]. This is also perfectly fine. However, in special cases this leads to ambiguities. Here is a short code example:

extern int index1;
extern int index2;
extern int array1[5];
extern int array2[5];
extern int array3[5];
extern int array4[5];

int main() {

  array1[index1] = array2[index2];

  array3[index1] = array4[index1];

  return 0;
}

[from] ====== DEPENDENCIES COMPUTED ======
  These dependencies hold at termination for the executions that terminate:
[from] Function main:
  array1[0..4] FROM index1; index2; array2[0..4] (and SELF)
  array3[0..4] FROM index1; array4[0..4] (and SELF)
  \result FROM \nothing
[from] ====== END OF DEPENDENCIES ======

This leads to the following dependencies. I read these as follows: Since the values of index1 and index2 are not known, all elements of array1 are dependent on all elements of array2. Like this:

array1[0] FROM array2[0]
array1[0] FROM array2[1]
...
array1[1] FROM array2[0]
array1[1] FROM array2[1]
...
array1[4] FROM array2[3]
array1[4] FROM array2[4]

In the second assignment, the index is also unknown, but the same index is used both times. Therefore, slightly different dependencies should also apply here. Like this:

array3[0] FROM array4[0]
array3[1] FROM array4[1]
array3[2] FROM array4[2]
array3[3] FROM array4[3]
array3[4] FROM array4[4]

The summarising representation using array[0..N] does not provide any detailed information here. Is there a way to output the dependencies element by element (as shown above) to prevent these ambiguities?

Solution

The From plug-in relies on the results from the Eva plug-in. However, with the current state of the plug-in, it is not possible to get the result that you expect. On the assignment:

array3[index] = array4[index]

We have index ∈ [0..4], thus it cannot compute anything more precise than: array3[0..4] FROM index; array4[0..4], thus something similar to the first example.