frama-c - 关于frama-c中数组的要求

Question

在frama-c中编写函数的ACSL时，我希望全局变量数组满足要求，例如：

int a[5];

/*@requires \forall int i; 0 <= i <= 4 ==> a[i] > 0;
*/
void f()
{
    do something with a...;
}

我想要一个大于 0 的所有元素，是吗？试了一下，还是不行，谁能告诉我怎么写？

非常感谢。

Answer 1

正如其手册中所解释的，值分析插件仅理解 ACSL 公式的一个子集。

特别是，它不处理量词，因此您的前置条件对结果状态没有影响。f通常的技巧是编写一个将在适当环境中调用的包装函数。为此，您可以特别使用该Frama_C_interval功能。例如，您的包装器可能是（不要忘记#include <limits.h>在您的文件中，因为INT_MAX）

void wrap() {
  for(int i=0; i<=4; i++) a[i] = Frama_C_interval(1,INT_MAX);
  f();
}

你会这样称呼 Frama-C：

frama-c -val -main wrap -lib-entry file.c