[splint.git] / test / fileio / filerw.c

int f (/*@open@*/ /*@read@*/ FILE *f1, /*@open@*/ /*@write@*/ FILE *f2)
{
  int c;

  c = fgetc (f1);
  c = fgetc (f2); /* error: not readable */
  
  (void) fputc ('a', f1); /* error */
  (void) fseek (f1, 0, SEEK_CUR); 
  (void) fputc ('a', f1); /* okay */
 
  c = fgetc (f1); /* error */
  return c;
}
Commit	Line	Data
80ee600a	1	int f (/@open@/ /@read@/ FILE f1, /@open@/ /@write@/ FILE f2)
80ee600a	2	{
60eced23	3	int c;
80ee600a	4
60eced23	5	c = fgetc (f1);
	6	c = fgetc (f2); /* error: not readable */
	7
	8	(void) fputc ('a', f1); /* error */
	9	(void) fseek (f1, 0, SEEK_CUR);
	10	(void) fputc ('a', f1); /* okay */
	11
	12	c = fgetc (f1); /* error */
	13	return c;
80ee600a	14	}