Frama-C acsl max example from manual not working

Question

I believe I am missing something obvious, but I have tried a lot and I haven't managed to find the source of the problem.

I am following the acsl guide from Frama-C. There is this introductory example of how to verify the correctness of finding the maximum value in an array:

/*@ requires n > 0;
    requires \valid(p+ (0 .. n-1));
    ensures \forall int i; 0 <= i <= n-1 ==> \result >= p[i];
    ensures \exists int e; 0 <= e <= n-1 && \result == p[e];
*/
int max_seq(int* p, int n) {
  int res = *p;
  for(int i = 0; i < n; i++) {
    if (res < *p) { res = *p; }
    p++;
  }
  return res;
}

However, running frama-c -wp -wp-prover alt-ergo samenum.c -then -report I get:

[wp] Warning: Missing RTE guards
[wp] samenum.c:8: Warning: Missing assigns clause (assigns 'everything' instead)
[wp] 2 goals scheduled
[wp] [Alt-Ergo] Goal typed_max_seq_ensures_2 : Timeout (Qed:1ms) (10s)
[wp] [Alt-Ergo] Goal typed_max_seq_ensures : Timeout (Qed:2ms) (10s)
[wp] Proved goals:    0 / 2
  Alt-Ergo:        0  (interrupted: 2)
[report] Computing properties status...

--------------------------------------------------------------------------------
--- Properties of Function 'max_seq'
--------------------------------------------------------------------------------

[    -    ] Post-condition (file samenum.c, line 3)
            tried with Wp.typed.
[    -    ] Post-condition (file samenum.c, line 4)
            tried with Wp.typed.
[    -    ] Default behavior
            tried with Frama-C kernel.

It seems that alt-ergo times out before proving the property. For what is worth, I tried with higher time-out but it still doesn't work.

I am using:

• frama-c: 19.1
• why3: 1.2.0
• alt-ergo: 2.3.2

I am running this on Ubuntu 18.04 and before running the command I run: why3 config --detect to make sure why3 knows about alt-ergo.

Any ideas? Can anyone verify that this is example is not working? Any help would be greatly appreciated!

Answer 1

This mini-tutorial was written quite a long time ago and is not really up to date. A new version of the website should appear in the upcoming months. Basically, this contract, as well as the invariant for the loop pointed by @iguerNL were meant to be verified using the Jessie plugin, and not the WP plugin of Frama-C. Among the differences between these two plugins, Jessie did not need assigns clauses for loops and functions, while WP needs them.

Thus, a complete annotated max_seq function could be this one:

/*@ requires n > 0; 
    requires \valid(p+ (0..n−1));
    assigns \nothing;
    ensures \forall int i; 0 <= i <= n−1 ==> \result >= p[i]; 
    ensures \exists int e; 0 <= e <= n−1 && \result == p[e]; 
*/ 
int max_seq(int* p, int n) { 
  int res = *p; 
  //@ ghost int e = 0; 
  /*@ loop invariant \forall integer j; 0 <= j < i ==> res >= \at(p[j],Pre); 
      loop invariant \valid(\at(p,Pre)+e) && \at(p,Pre)[e] == res; 
      loop invariant 0<=i<=n; 
      loop invariant p==\at(p,Pre)+i; 
      loop invariant 0<=e<n; 
      loop assigns i, res, p, e;
      loop variant n-i;
  */ 
  for(int i = 0; i < n; i++) { 
    if (res < *p) { 
      res = *p; 
      //@ ghost e = i; 
    }
    p++; 
  } 
  return res; 
}

where we specify that the functions does not assign anything in memory, and that the loop assigns the different local variables i, res, p and e (thus leaving n unchanged).

Note that more recent tutorials are available to learn about the use of Frama-C with the WP plugin. The future version of the Frama-C website mentions:

• A comprehensive tutorial on ACSL and WP
• Another tutorial, with specifications inspired notably from C++ containers

Answer 2

You probably forgot to add invariants for the "for" loop. See Section "10.2 Loop Invariants" in the manual you gave (https://frama-c.com/acsl_tutorial_index.html)