test/conditions/miroslaw.c

   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 }