test/conditions/releases.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(/*@only@*/ /*@notnull@*/ ipp This) ;
  12
  13 void ipp_delete(ipp This)
  14 {
  15   free(This); /* should be error for not deleting This->ip! */
  16 }