#include<vcc.h>
#include<limits.h>

/*
// Need for loop invariant
void foo() 
  _(requires \true)
{
  // _(assume \true);
  int x = 0;
  while (x < 10)
    _(invariant x <= 12)
  {
    x = x + 1;
  }
  _(assert x == 10);
}


// Asserts after a failing assert
void foo()
{
  int x, y;
  _(assert x > 0);
  _(assert x > -1);
}


// Assume
void baz()
{
  int x, y;
  _(assume x < y)
  _(assert x+1 < y+1)
}

*/


// Overflow and _(unchecked)
// VCC treats expresssions as having normal arithmetic meaning
// unlike expressions in assignments etc, which can overflow;
// but will warn you of possible overflow.
// _(unchecked) is a type-cast that means "evaluate using overflows and assign to LHS"
void bar()
{
  unsigned int a, b;
  _(assume b < UINT_MAX);
  a = _(unchecked) (b + 1);
  _(assert a > b)
    // _(assume a == b);
    // a = _(unchecked) a++;
  // b = _(unchecked) b++;
  // _(assert a == b);
  // Does not verify!
  // _(assert (a == 0 || a > b));
}