test/fileio/filerw.xh

   1 extern /*@rweither@*/ FILE *fopen (const char *filename, const char *mode) ;
   2
   3 extern int fgetc (/*@read@*/ FILE *f) ;
   4 extern int fputc (int, /*@write@*/ FILE *f) ;
   5
   6 /* fseek resets the rw state of a stream */
   7 int fseek (/*@rweither@*/ FILE *stream, long int offset, int whence)
   8   /*@ensures rweither stream@*/ ;
   9
  10