Frama-c 无法证明 goto 实现的循环

Question

• 环境：24.0（铬）
• 命令：frama-c -wp -wp-legacy xx.c

#include <stdlib.h>
int r;
/*@
  requires \valid_read(a + (0 .. length-1)) && length > 0;
  assigns r;
  ensures \forall size_t off ; 0 <= off < length ==> a[off] != r;
*/
void notin(int* a, size_t length) {
  int result = 0;
  int max = 0;
  size_t i = 0;
  
assign_part:
  if (a[i] >= max) {
    max = a[i];
  }
  result = max + 1;
  i = i + 1;
 
  if (i < length) {
    goto assign_part;
  }

  r = result;
}

错误消息显示：

[kernel] Parsing goto_test/while_2_goto_version.c (with preprocessing)
[wp] Warning: Missing RTE guards
[wp] goto_test/while_2_goto_version.c:14: Warning: 
  Missing assigns clause (assigns 'everything' instead)
[wp] 6 goals scheduled
[wp] [Alt-Ergo ] Goal typed_notin_assigns_part2 : Timeout (Qed:4ms) (10s)
[wp] Proved goals:    5 / 6
  Qed:             4  (3ms-10ms-30ms)
  Alt-Ergo :       1  (6ms) (44) (interrupted: 1)
[wp] goto_test/while_2_goto_version.c:8: Warning: 
  Memory model hypotheses for function 'notin':
  /*@ behavior wp_typed:
        requires \separated(a + (..), &r

用 while 循环实现的等效代码可以通过

frama-c

证明：

#include <stdlib.h>
int r;
/*@
  requires \valid_read(a + (0 .. length-1)) && length > 0;
  assigns r;
  ensures \forall size_t off ; 0 <= off < length ==> a[off] != r;
*/
void notin(int* a, size_t length) {
 int result = 0;
 int max = 0;
 size_t i = 0;
 
 /*@ loop invariant 0 <= i <= length;
   @ loop invariant \forall size_t j; 0 <= j < i ==> a[j] <= max;
   @ loop invariant \forall size_t k; 0 <= k < i ==> a[k] != result;
   @ loop assigns i, result, max;
 */
 while (i < length) {
   if (a[i] >= max) {
     max = a[i];
   }
   result = max + 1;
   i = i + 1;
 }

 r = result;
}

Answer 1

从 Frama-C 23 开始，使用

gotos

实现的循环（称为“非自然循环”）的支持已被删除。主要是因为旧的WP引擎可能是错误的。这是 WP 手册（第 1.6 节）中列出的已知限制：

https://frama-c.com/download/wp-manual-28.0-Nickel.pdf

在新的 WP 引擎中添加此支持是可能的，但需要大量工作。