int x = 10;
  while (x --> 0) {
    printf("%d ", x);
  }