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

    ensures \forall integer i; 0 <= i < n ==> a[i] == 0;

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

/* Essais sur le assigns (mal-géré par le wp dans les dernières versions).

This seems due to the fact that in some cases, for a sequence "S1; S2"
WP checks assigns clause is satisfied in both S1 and S2, but with too
weak hypotheses for S2 (there is not the full strongest-postcondition
of S1 in the context).

 */

int i;
int t[10];

/*@ assigns i,t[\at(i,Post)];
  @ ensures 0<=i<10 && t[i]==\old(t[\at(i,Post)])/2;
*/
void test1() {
  i=10/2;
  t[i]=t[i]/2;
}

/* BUG OF FRAMA-C / WP 
 
 Below a variant of "test1" where "t" is in arguments ! 
 */

/*@ requires \valid(t+(0..10-1)) && \separated(&i,t+(0..10-1));
  @ assigns i,t[\at(i,Post)];
  @ ensures  0<=i<10 && t[i]==\old(t[\at(i,Post)])/2;
*/
void test2(int *t) {
  i=10/2;
  t[i]=t[i]/2;  /* unprovable VC-assigns here ! */
}