Frama-C 警告：缺少分配子句（改为分配“所有内容”）答案

【问题标题】：Frama-C warning: Missing assigns clause (assigns 'everything' instead)Frama-C 警告：缺少分配子句（改为分配“所有内容”）
【发布时间】：2018-04-12 18:30:57
【问题描述】：

我正在用 frama-c 测试这个小程序，但我一直收到同样的错误。我不确定这意味着什么。我对分配一切意味着什么感到特别困惑。

这是带有 ACSL 注释的代码：

// assuming n is nonnegative and even, f returns n

/*@ requires n>=0;
*/

int f(int n) {
  int i=0;
  while (i<n) {
    i+=2;
  }
  //@ assert i==n;
  return i;
}

这是我尝试测试代码时终端所说的内容：

[wp] warning: Missing RTE guards
p3.c:9:[wp] warning: Missing assigns clause (assigns 'everything' instead)
[wp] 1 goal scheduled
[wp] [Alt-Ergo] Goal typed_f_assert : Unknown (Qed:8ms) (54ms)
[wp] Proved goals:    0 / 1
    Alt-Ergo:        0  (unknown: 1)

【问题讨论】：

标签： automated-tests frama-c acsl

【解决方案1】：

首先，您的属性不正确，因为您不需要 n 甚至在函数的前提条件中。因此，我将向您展示如何在循环体中使用 i += 1 来证明您的程序的变体。

assigns 子句是 WP 要求您为每个循环和每个外部函数调用指定的内容。它必须包含可以被循环（或函数）修改的所有内存位置（即变量）的列表。它需要这个才能知道其他所有内容都没有被循环修改。特别是，在这个程序中，WP 需要知道，虽然i 的值可能会在循环中改变，但n 的值不会改变。但如果你不告诉它是这种情况，它会假定循环可能会分配“一切”，包括n。

要指定这一点，您可以在循环上方插入以下注释：

/*@ loop assigns i; */

如果您尝试证明这一点（在 GUI 中），您将看到 WP 可以验证此 assigns 子句。

但是，你在循环之后的断言仍然不能用这个来证明。这是因为除了 assigns 子句之外，每个循环还必须有一个 循环不变量：在循环的每次迭代之前和之后始终为真的东西。选择正确且足够强大的循环不变量是一门黑暗的艺术，但一般来说，不变量必须是这样的，一旦循环条件为假并且循环终止，我们就可以在循环之后得出断言。

也就是说，我们希望公式I 具有以下属性：

I && !(i < n)  ==>  i == n

因此，一个不错的选择是循环不变量i <= n，因为如果i <= n 但我们知道i < n 不是 true（因为循环已停止迭代），那么i 必须等于n。

将所有内容放在一起，这是您的程序的注释变体：

/*@ requires n>=0;
*/

int f(int n) {
  int i=0;
  /*@ loop assigns i;
    @ loop invariant i <= n;
   */
  while (i<n) {
    i += 1;
  }
  //@ assert i==n;
  return i;
}

这是自动验证的：

[wp] warning: Missing RTE guards
[wp] 4 goals scheduled
[wp] Proved goals:    4 / 4
    Qed:             4

【讨论】：