手册中的 Frama-C acsl max 示例不起作用

Question

我相信我遗漏了一些明显的东西，但我已经尝试了很多，但我还没有设法找到问题的根源。

我正在关注来自 Frama-C 的 acsl guide。有一个关于如何验证在数组中找到最大值的正确性的介绍性示例：

/*@ requires n > 0;
    requires \valid(p+ (0 .. n-1));
    ensures \forall int i; 0 <= i <= n-1 ==> \result >= p[i];
    ensures \exists int e; 0 <= e <= n-1 && \result == p[e];
*/
int max_seq(int* p, int n) {
  int res = *p;
  for(int i = 0; i < n; i++) {
    if (res < *p) { res = *p; }
    p++;
  }
  return res;
}

然而，运行宁frama-c -wp -wp-prover alt-ergo samenum.c -then -report我得到：

[wp] Warning: Missing RTE guards
[wp] samenum.c:8: Warning: Missing assigns clause (assigns 'everything' instead)
[wp] 2 goals scheduled
[wp] [Alt-Ergo] Goal typed_max_seq_ensures_2 : Timeout (Qed:1ms) (10s)
[wp] [Alt-Ergo] Goal typed_max_seq_ensures : Timeout (Qed:2ms) (10s)
[wp] Proved goals:    0 / 2
  Alt-Ergo:        0  (interrupted: 2)
[report] Computing properties status...

--------------------------------------------------------------------------------
--- Properties of Function 'max_seq'
--------------------------------------------------------------------------------

[    -    ] Post-condition (file samenum.c, line 3)
            tried with Wp.typed.
[    -    ] Post-condition (file samenum.c, line 4)
            tried with Wp.typed.
[    -    ] Default behavior
            tried with Frama-C kernel.

似乎 alt-ergo 在证明属性之前超时了。值得一提的是，我尝试了更高的超时时间，但仍然无效。

我正在使用：

frama-c: 19.1
why3: 1.2.0
alt-ergo: 2.3.2

我运行在 Ubuntu 18.04 和运行之前运行执行命令 I 运行: why3 config --detect 以确保 why3 知道 alt -ergo.

有什么想法吗？任何人都可以验证这个例子不起作用吗？任何帮助将不胜感激！

Answer 1

您可能忘记为 "for" 循环添加不变量。请参阅您提供的手册中的“10.2 循环不变量”部分 (https://frama-c.com/acsl_tutorial_index.html)

Answer 2

这个迷你教程是很久以前写的，并不是最新的。该网站的新版本应该会在未来几个月出现。基本上，这个合同，以及@iguerNL 指向的循环的不变量，是为了使用 Jessie 插件而不是 Frama-C 的 WP 插件来验证的。在这两个插件的区别中，Jessie 不需要 assigns 循环和函数的子句，而 WP 需要它们。

因此，一个完整的注释 max_seq 函数可能是这个：

/*@ requires n > 0; 
    requires \valid(p+ (0..n−1));
    assigns \nothing;
    ensures \forall int i; 0 <= i <= n−1 ==> \result >= p[i]; 
    ensures \exists int e; 0 <= e <= n−1 && \result == p[e]; 
*/ 
int max_seq(int* p, int n) { 
  int res = *p; 
  //@ ghost int e = 0; 
  /*@ loop invariant \forall integer j; 0 <= j < i ==> res >= \at(p[j],Pre); 
      loop invariant \valid(\at(p,Pre)+e) && \at(p,Pre)[e] == res; 
      loop invariant 0<=i<=n; 
      loop invariant p==\at(p,Pre)+i; 
      loop invariant 0<=e<n; 
      loop assigns i, res, p, e;
      loop variant n-i;
  */ 
  for(int i = 0; i < n; i++) { 
    if (res < *p) { 
      res = *p; 
      //@ ghost e = i; 
    }
    p++; 
  } 
  return res; 
}

我们指定函数不在内存中分配任何内容，并且循环分配不同的局部变量 i、res、p 和 e （因此 n 保持不变）。

请注意，可以使用更多最新教程来了解如何将 Frama-C 与 WP 插件一起使用。未来版本的Frama-C网站提到：

手册中的 Frama-C acsl max 示例不起作用

Frama-C acsl max example from manual not working

frama-c

alt-ergo