[splint.git] / test / conditions / releases.c

#include <stdlib.h>

typedef struct ipp_s *ipp;

struct ipp_s
{
  /*@only@*/ /*@notnull@*/
  int *ip;
} ;

extern void ipp_delete(/*@only@*/ /*@notnull@*/ ipp This) ;

void ipp_delete(ipp This)
{
  free(This); /* should be error for not deleting This->ip! */
}
Commit	Line	Data
80ee600a	1	#include <stdlib.h>
	2
	3	typedef struct ipp_s *ipp;
	4
	5	struct ipp_s
	6	{
	7	/@only@/ /@notnull@/
	8	int *ip;
	9	} ;
	10
	11	extern void ipp_delete(/@only@/ /@notnull@/ ipp This) ;
	12
	13	void ipp_delete(ipp This)
	14	{
	15	free(This); /* should be error for not deleting This->ip! */
	16	}