1extern 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@*/ ;
5
6extern /*@open@*/ FILE *fopen (const char *filename, const char *mode)
7   /*
8   ** File modes:
9   **       "rb"	read
10   **       "wb"        create, truncate, write
11   **       "ab"        create, write, append
12   **       "rb+"	read, write
13   **       "wb+"	create, truncate, read, write
14   **       "ab+"	create, read, write, append
15   */
16   ;
17
18extern /*@open@*/ FILE *freopen (char *filename, char *mode, /*@closed@*/ FILE
19*stream) /*@ensures open stream@*/ ;
20
21extern /*@null@*/ char *
22  fgets (/*@returned@*/ /*@out@*/ char *s, int n, /*@open@*/ FILE *stream)
23  /*@modifies fileSystem, *s, *stream, errno@*/ ;
24
25/*
26fgetc
27fputc
28
29fseek
30ftell
31*/
32
33int ferror (FILE *stream) ;
34int feof (FILE *stream) ;
35void clearerr (FILE *stream) ;
36