test/fileio/file.c

   1 extern FILE *f1;
   2
   3 FILE *f (FILE *fin, FILE *fout)
   4      /*@ensures closed fin@*/
   5 {
   6   FILE *res;
   7   int x;
   8
   9   x = fgetc (fin);
  10
  11   if (x > 65)
  12     {
  13       (void) fclose (fout);
  14     } /* merge incompatible */
  15
  16   if (x > 65)
  17     {
  18       ;
  19     }
  20   else
  21     {
  22       (void) fclose (fin);
  23     } /* merge incompatible */
  24
  25   return res;
  26 }