Frama-C无法验证goto实现的循环，while版本可正常验证

环境与验证命令 #

• 环境：Frama-C 24.0（基于Chromium）
• 验证命令：frama-c -wp -wp-legacy xx.c

goto循环实现代码（无法完成验证） #

#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循环等价代码（验证成功） #

#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;
}

原因分析与修复建议 #

Frama-C的WP插件对结构化循环（如while）的支持更完善：while版本通过loop invariant明确了循环过程中始终成立的性质，loop assigns指定了循环内会修改的变量，这些注解大幅减少了验证器需要探索的证明路径，从而顺利完成验证。

而goto形成的非结构化循环，WP无法自动识别并推导循环不变式；同时代码中缺少对goto循环内修改变量的assigns注解（错误信息也明确提示了"Missing assigns clause"），导致验证器需要尝试大量可能性，最终超时。

要让goto版本通过验证，只需手动添加对应的循环注解，在assign_part:标签前补充如下内容即可：

/*@ 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;
*/

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