/*@
  assigns \nothing;
  ensures -10 < \result < 10;
*/
int bar();


/*@
   assigns \nothing;
   ensures \result >= -10;
*/
int foo()
{
   return 3+bar();
}