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

extern FILE *f1;

FILE *f (FILE *fin, FILE *fout)
     /*@ensures closed fin@*/
{
  FILE *res;
  int x;

  x = fgetc (fin);

  if (x > 65)
    {
      (void) fclose (fout);
    } /* merge incompatible */

  if (x > 65)
    {
      ;
    }
  else
    {
      (void) fclose (fin);
    } /* merge incompatible */

  return res;
}
Commit	Line	Data
68de3f33	1	extern FILE *f1;
	2
	3	FILE f (FILE fin, FILE *fout)
	4	/@ensures closed fin@/
	5	{
	6	FILE *res;
	7	int x;
	8
	9	x = fgetc (fin);
	10
	11	if (x > 65)
	12	{
	13	(void) fclose (fout);
	14	} /* merge incompatible */
	15
	16	if (x > 65)
	17	{
	18	;
	19	}
	20	else
	21	{
	22	(void) fclose (fin);
	23	} /* merge incompatible */
	24
	25	return res;
	26	}