Frama-C from插件数组依赖歧义：如何逐元素输出依赖关系？

问题背景 #

使用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的所有元素
• 第二个赋值中，左右索引均为index1，array3的每个元素仅依赖array4对应索引的元素，但汇总输出无法体现这种区别

解决方案 #

添加-from-array-elements参数调用Frama-C，强制插件逐元素输出数组依赖，消除汇总歧义。

执行命令：

frama-c -from-array-elements your_code.c

对应输出示例：

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

该输出清晰区分了两种场景的依赖关系：array1的每个元素都依赖array2的全部元素，而array3的每个元素仅关联array4对应位置的元素，完全匹配预期逻辑。

若需要禁止所有依赖汇总（不止数组），可结合使用-from-no-collapse参数，但-from-array-elements更针对性地解决数组元素的汇总歧义问题。

内容的提问来源于stack exchange，提问作者Gruber