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

#include <stdlib.h>

typedef struct ipp_s *ipp;

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

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

void ipp_delete(ipp This)
{
  free(This);
}
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(/@special@/ /@only@/ /@notnull@/ ipp This)
	12	/@releases This@*/;
	13
	14	void ipp_delete(ipp This)
	15	{
	16	free(This);
	17	}