The example in this question seems to work only for fixed-length arrays, however the similar code below from https://frama-c.com/html/acsl.html doesn't seem to pass. As soon as I change the code to be include the requirement && n == 42 (or any other positive integer) it passes.

When it fails it says [wp] [Alt-Ergo 2.4.1] Goal typed_set_to_0_loop_invariant_established : Timeout (Qed:1ms) (1') (cached)

/*@
  requires \valid(a (0..n-1));

  assigns  a[0..n-1];

  ensures

  \forall integer i;
    0 <= i < n ==> a[i] == 0;
*/
void set_to_0(int* a, int n){
  int i;

  /*@
    loop invariant 0 <= i <= n;
    loop invariant
    \forall integer j;
      0 <= j < i ==> a[j] == 0;
    loop assigns i, a[0..n-1];
    loop variant n-i;
  */
  for(i = 0; i < n;   i)
    a[i] = 0;
}

Any tips on how to proceed / what the intended behaviour/flags are?

CodePudding user response：

Actually, the loop invariant 0 <= i <= n is not true if n is strictly negative. A loop invariant must hold the first time you reach the loop (this is what the "established" part means, as opposed to the "preserved" part in which you must check that it holds at the end of any loop step, assuming it was true at the beginning of said step), even if you don't end up entering the loop at all (which is obviously the case here if n<0). You must thus add a requires n >=0; in the contract of the function.

EDIT I forgot to mention that another solution is of course to make n and i unsigned (or even better to #include <stddef.h> and use size_t): this way, you are guaranteed a positive number without having to write an additional requires)