• 环境：24.0（ chrome ）
• 命令：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;
}

型