]>
Commit | Line | Data |
---|---|---|
990ec868 | 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 |