[splint.git] / test / deadparam.c

extern void f (/*@out@*/ char *s);
extern void g (/*@special@*/ char *s) /*@allocates s@*/ ;

void t (/*@only@*/ char *s1, /*@only@*/ char *s2)
{
  free (s1);
  f (s1);

  free (s2);
  g (s2);
}
Commit	Line	Data
80ee600a	1	extern void f (/@out@/ char *s);
	2	extern void g (/@special@/ char s) /@allocates s@*/ ;
	3
	4	void t (/@only@/ char s1, /@only@/ char s2)
	5	{
	6	free (s1);
	7	f (s1);
	8
	9	free (s2);
	10	g (s2);
	11	}