extern int a;

/*@
   assigns a;
   ensures a == c;
*/
void foo(int b)
{
    a = b;
}