解决数组依赖关系

Question

我目前正在使用 Frama-C 和 from 插件来获取变量之间的依赖关系。如果数组的多个元素具有相同的依赖性，则会以摘要形式输出，如下所示：

array[0..N]

。 这也完全没问题。然而，在特殊情况下，这会导致歧义。这是一个简短的代码示例：

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 ======

这会导致以下依赖关系。我读了这些内容如下： 由于index1 和index2 的值未知，因此array1 的所有元素都依赖于array2 的所有元素。 像这样：

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]

在第二次分配中，索引也是未知的，但两次使用了相同的索引。因此，稍微不同的依赖关系也应该适用于此。 像这样：

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]

使用

array[0..N]

的总结表示此处不提供任何详细信息。有没有办法逐个元素输出依赖关系（如上所示）以防止这些歧义？

Answer 1

From 插件依赖于 Eva 插件的结果。但是，以插件的当前状态，不可能获得您期望的结果。关于作业：

array3[index] = array4[index]

我们有

index ∈ [0..4]

，因此它无法计算出比：

array3[0..4] FROM index; array4[0..4]

更精确的东西，因此与第一个示例类似。