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