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?