Frama-C/WP tutorial example "mismatch algorithm"

Question

I am trying the WP tutorial examples with Frama-C (Neon-20140301) and Alt-Ergo. I got stuck with the "mismatch algorithm" example while other similar examples such as "equal" and "find" have no problems. The code is listed below. The post conditions P0, P2 are not being discharged. Can anyone tell me what is wrong here?

#include<stdbool.h>

/*@
  @ predicate IsEqual {A,B} (float* a, integer n, float* b) =
  @   \forall integer i; 0 <= i < n ==> \at(a[i], A) == \at(b[i], B);
*/a

/*@ requires n >= 0;
  @ requires \valid(a+(0..n-1));
  @ requires \valid(b+(0..n-1));
  @ 
  @ assigns \nothing;
  @ 
  @ behavior all_equal:
  @   assumes IsEqual{Here,Here}(a, n, b);
  @   ensures P0: \result == n;
  @   
  @ behavior some_not_equal:
  @   assumes !IsEqual{Here,Here}(a, n, b);
  @   ensures P1: 0 <= \result < n;
  @   ensures P2: a[\result] != b[\result];
  @   ensures P3: IsEqual{Here,Here}(a, \result, b);
  @   
  @ complete behaviors;
  @ disjoint behaviors;
*/

bool mismatch (float* a, int n, float* b)
{
  /*@ loop invariant 0 <= i <= n;
    @ loop invariant IsEqual{Here,Here}(a, i, b);
    @ loop assigns i;
    @ loop variant n-i;
   */
  for (int i=0; i<n; i++) {
    if (a[i] != b[i])
      return i;
  }
  return n;
}

Answer 1

Your function is supposed to return a bool, i.e. either 0 or 1. Any integral value x can be converted to _Bool: the boolean is 0 if x==0 and 1 otherwise (see C99 and C11 section 6.3.1.2). If you look at the code as normalized by Frama-C, this is exactly what is being done for return i and return n. There is thus no reason that \result should be equal to n or an index at which both arrays differ. If you make your function returning an int instead, everything is discharged by Alt-ergo.