test/refcounts.c

   1 extern /*@out@*/ /*@only@*/ void *smalloc (size_t);
   2
   3 typedef /*@refcounted@*/ struct _rp
   4 {
   5   /*@refs@*/ int refs;
   6   /*@only@*/ int *p;
   7 } *rp;
   8
   9 extern rp rp_create2 (void);
  10
  11 void rp_release (/*@killref@*/ rp x)
  12 {
  13   x->refs--;
  14
  15   if (x->refs == 0)
  16     {
  17       free (x->p);
  18       free (x); /* 1. Reference counted storage passed as only param: free (x) */
  19     }
  20 }
  21
  22 /*@tempref@*/ rp rp_temp (void)
  23 {
  24   return rp_create2 (); /* 2. New reference returned as temp reference: rp_create2() */
  25 }
  26
  27 void rp_f (/*@killref@*/ rp r1, /*@killref@*/ rp r2)
  28 {
  29   rp rt = rp_temp ();
  30
  31   rp_release (r1);
  32   r2 = rp_temp (); /* 3. Kill reference parameter r2 not released before assignment */
  33   rp_release (rt);
  34 }
  35
  36 rp rp_create (/*@only@*/ int *p)
  37 {
  38   rp r = (rp) smalloc (sizeof(rp));
  39
  40   r->refs = 1;
  41   r->p = p;
  42
  43   return r;
  44 }
  45
  46 rp rp_ref (rp x)
  47 {
  48   return x; /* 4. Reference counted storage returned without modifying ... */
  49 }
  50
  51 rp rp_refok (rp x)
  52 {
  53   x->refs++;
  54   return x;
  55 }
  56
  57 rp rp_waste (/*@only@*/ int *p)
  58 {
  59   rp z1 = rp_create (p);
  60   rp z2 = rp_ref (z1);
  61
  62   z2->p++;
  63   return z1; /* 5. New reference z2 not released before return */
  64 }
  65
  66 rp rp_waste2 (/*@only@*/ int *p)
  67 {
  68   rp z1 = rp_create (p);
  69   rp z2 = rp_ref (z1);
  70
  71   z2 = rp_ref (z1); /* 6. New reference z2 not released before assignment */
  72   return z1; /* 7. New reference z2 not released ... */
  73 }
  74
  75