Frama-c cannot prove loop implemented by goto

Env: 24.0 (Chromium)
Command: 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;
}

The error message says:

[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

The equivalent code implemented with while loop which can be proved by 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;
}

Solution

From Frama-C 23, the support of loops implemented using gotos (called "non-natural loops") has been removed. Mainly because it was probably wrong in the old WP engine. This is a known limitation that is listed in the manual of WP (Section 1.6):

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

Adding this support in the new WP engine is possible but requires substantial work.

Now, what are the problems here. First, the property that it not proved is the global assigns property. The reason why it is not proved is that when the old WP engine finds that there is a loop with goto, it considers that it assigns everything (which is more than just r). One would have to provide an assigns specification for the loop. However, after diving into the code of the engine, I am pretty sure that there is no way to provide such a specification for a loop with gotos.

Second, to prove a code that contains a loop, WP needs a suitable invariant. Here, we have no "classic" loop, thus one cannot provide a loop invariant, we should thus use a generalized invariant:

L:
  //@ invariant ...
  foo();
goto L;

However, again, this is not supported in the WP engines (both the old and the new one).