test/fileio/filerw.c

   1 int f (/*@open@*/ /*@read@*/ FILE *f1, /*@open@*/ /*@write@*/ FILE *f2)
   2 {
   3   int c;
   4
   5   c = fgetc (f1);
   6   c = fgetc (f2); /* error: not readable */
   7
   8   (void) fputc ('a', f1); /* error */
   9   (void) fseek (f1, 0, SEEK_CUR);
  10   (void) fputc ('a', f1); /* okay */
  11
  12   c = fgetc (f1); /* error */
  13   return c;
  14 }