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

// _(unchecked) (exp) means evaluate "exp" using type semantics of C.
// VCC gives a warning if it thinks evaluating "exp" may oveflow or assigning to LHS may overflow.
// Without _(unchecked), VCC evaluates as unbounded integers, but still gives overflow error if it feels "exp" may overflow its type.


// post condition verifies, but gives possible overflow error
unsigned int foo (unsigned int x)
_(ensures \result > x)
{
  return (x + 1);
}

// No overflow error (because "unchecked" says bounded arithmetic intended), but post condition does not verify
unsigned int foo1 (unsigned int x)
_(ensures \result > x)
{
  return _(unchecked) (x + 1);
}


// post condition verifies, no overflow error
unsigned int foo2 (unsigned int x)
_(requires x < UINT_MAX)
_(ensures \result > x)
{
  return _(unchecked) (x + 1);
}

// post condition verifies, no overflow error
unsigned int foo3 (unsigned int x)
_(requires x < UINT_MAX)
_(ensures \result > x)
{
  return (x + 1);
}