int min, max;

/*@ 
  requires min <= max ;
  assigns \nothing;
  ensures min <= \result <= max ;
  ensures (min <= x <= max) ==> (\result == x) ;
*/
int saturation(int x)
{
  int res;
  if (x <= min) 
    res = min;
  else if (x >= max)
    res = max;
  else res = x;
  return res;
}