#include 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); }