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

// VCC will check each sub-expression for (under/)overflow using the type bounds from limits.h. If it can't conclude that expression is within limits it gives an "might overflow" error. As for assertions (including postconditions), it uses the overflow semantics of C when it is specified (like for unsigned int) and sees if the assertion verifies. If overflow semantics not specified (like in int), it says unable to verify.

// Gives possible overflow error, post condition does not verify
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);
}

// No overflow error (because "unchecked" says bounded arithmetic intended), and post condition verifies using overflow semantics for unsigned int 
unsigned int foo2 (unsigned int x)
_(ensures \result > x || \result == 0)
{
  return _(unchecked) (x + 1);
}


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

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

// post condition verifies, no overflow error
int foo5 (int x)
_(requires \true)
//_(ensures \result <= INT_MAX)
  _(ensures \result == x + 1 || \result == INT_MIN) does not verify as C semantics unspecified for int overflows
{
  return _(unchecked) (x + 1);
}