/*
 * This program demonstrates that a loop invariant need not hold after
 * normal termination of a for-loop, if its condition has side-effects.
 * 
 * The global variable j is treated in the same way as 
 * the local (to main()) variable i:
 * both are initialized to 0 (line 41, 46),
 * and then incremented repeatedly in the loop (line 34/46, 46).
 * 
 * In fact, the invariant j==i can be proven (line 44).
 * 
 * However, right after the loop, an unsatisfiable obligation of the form
 * "(...something satisfiable...) ==> i+1 == i"
 * is generated for the assert in line 48.
 * 
 * In fact, "i=5 j=6" is printed to stdout,
 * when the #include and the printf is uncommented.
 */



//#include <stdio.h>

static int j;

/*@ requires j < 100;
    assigns j;
    ensures j == \old(j) + 1;
    ensures \result == x;
*/
static int f(int x)
{
    ++j;
    return x;
}

int main(void)
{
    int i;
    j = 0;
    /*@ loop variant 5 - i;
	loop invariant 0 <= i <= 5;
	loop invariant j == i;
    */
    for (i=0; f(i)<5; ++i)
	;
    /*@ assert j == i; */
    //printf("i=%d j=%d\n",i,j);
    return 0;
}