test/compdestroy.c

   1 typedef /*@only@*/ int *oip;
   2
   3 typedef /*@abstract@*/ struct
   4 {
   5   oip *ips;
   6   int size;
   7 } *sip;
   8
   9 void sip_free (/*@only@*/ sip x)
  10 {
  11   int i;
  12
  13   for (i = 0; i < x->size; i++)
  14     {
  15       free (x->ips[i]);
  16       free (x->ips[i]);
  17     }
  18
  19   free (x->ips);
  20   free (x);
  21 }
  22
  23 void sip_free2 (/*@only@*/ sip x)
  24 {
  25   free (x->ips); /* 1. Only storage *(x->ips) (type oip) derived from released */
  26   free (x);
  27 }
  28