/* Generated by Frama-C */
int main(int i)
{
  int x = i;
  if (i > 8) x = 8;
  return x;
}