[splint.git] / test / metastate / file.xh

extern int fclose (/*@open@*/ FILE *stream) 
   /*@ensures closed stream@*/ ;

extern /*@open@*/ FILE *fopen (char *filename, char *mode) ;

extern /*@open@*/ FILE *freopen (char *filename, char *mode, /*@closed@*/ FILE
*stream) /*@ensures open stream@*/ ;

extern /*@null@*/ char *
  fgets (/*@returned@*/ /*@out@*/ char *s, int n, /*@open@*/ FILE *stream)
  /*@modifies fileSystem, *s, *stream, errno@*/ ;
Commit	Line	Data
80ee600a	1	extern int fclose (/@open@/ FILE *stream)
	2	/@ensures closed stream@/ ;
	3
	4	extern /@open@/ FILE fopen (char filename, char *mode) ;
	5
	6	extern /@open@/ FILE freopen (char filename, char mode, /@closed@*/ FILE
	7	stream) /@ensures open stream@*/ ;
	8
	9	extern /@null@/ char *
	10	fgets (/@returned@/ /@out@/ char s, int n, /@open@/ FILE stream)
	11	/@modifies fileSystem, s, stream, errno@/ ;