[splint.git] / test / manual / only.c

extern /*@only@*/ int *glob;
 
/*@only@*/ int *
  f (/*@only@*/ int *x, int *y,
     int *z)
  /*@globals int *glob;@*/
{
  int *m = (int *)
    malloc (sizeof (int));
  
  glob = y;
  free (x);
  *m = *x;
  return z;
}
Commit	Line	Data
77970e15	1	extern /@only@/ int *glob;
	2
	3	/@only@/ int *
	4	f (/@only@/ int x, int y,
	5	int *z)
	6	/@globals int glob;@*/
	7	{
	8	int m = (int )
	9	malloc (sizeof (int));
	10
	11	glob = y;
	12	free (x);
	13	m = x;
	14	return z;
	15	}