1 extern int fclose (/*@open@*/ FILE *stream)
2 /*:checkerror EOF@*/ /* The fclose function returns zero if the
3 stream was successfully closed or EOF if any errors were detected. */
4 /*@ensures closed stream@*/ ;
6 /*@open@*/ FILE *fopen (const char *filename, const char *mode);
7 /*@open@*/ FILE *fdopen (int fildes, const char *mode);
12 ** "wb" create, truncate, write
13 ** "ab" create, write, append
15 ** "wb+" create, truncate, read, write
16 ** "ab+" create, read, write, append
19 extern /*@open@*/ FILE *freopen (char *filename, char *mode, /*@anyopen@*/ FILE *stream) /*@ensures open stream@*/ ;
21 extern /*@null@*/ char *
22 fgets (/*@returned@*/ /*@out@*/ char *s, int n, /*@open@*/ FILE *stream)
23 /*@modifies fileSystem, *s, *stream, errno@*/ ;
33 int ferror (FILE *stream) ;
34 int feof (FILE *stream) ;
35 void clearerr (FILE *stream) ;