int main(int argc, char **argv) {
  /*@ assert \forall integer i; 0 <= i < argc ==> \valid(argv[i]) ; */
  return 0;
}