int t[8];

/* Q0: Write the assigns clause in the contracts of functions init, incr, main.
   Q1: Verify the safety of function init.
   Q2: Verify the ACSL contract of function init. */

/*@ 
  ensures \forall integer i ; (0 <= i <= 7) ==> (t[i] == 1) ;
*/
void init(void)
{
  int i;
  for(i = 0; i < 8; i++)
    t[i] = 1;
}


/* Q3: Verify the safety of function incr.
   Q4: Verify the ACSL contract of function incr. */

/*@ 
  requires \forall integer i ; (0 <= i <= 7) ==> (t[i] == 1) ;
  ensures \forall integer i ; (0 <= i <= 7) ==> (t[i] == 2) ;
*/
void incr(void)
{
  int i;
  for(i = 7; i >= 0; i--)
    {
      t[i] += 1;
    }
}


/* Q5: Verify the ACSL contract of function main. */

/*@ 
  ensures \forall integer i ; (0 <= i <= 7) ==> (t[i] == 2) ;
*/
void main(void)
{
  init();
  incr();
}