test/sharing2.c

   1 extern /*@out@*/ /*@only@*/ void *smalloc (unsigned int size);
   2
   3 typedef int mint;
   4
   5 typedef struct _st
   6 {
   7   int a;
   8   /*@only@*/ int *b;
   9   /*@shared@*/ mint *c;
  10   int d;
  11 } *st;
  12
  13 /*@only@*/ st st_create1 ()
  14 {
  15   st res = (st) smalloc (sizeof(struct _st));
  16   int *z;
  17
  18   res->a = 3;
  19   z = res->b;   /* res->b not defined */
  20   z = (*res).c; /* (*res).c not defined */
  21
  22   return res;   /* res->d not defined */
  23 }
  24
  25 void f1(/*@only@*/ st x)
  26 {
  27   free (x->b);
  28   free (x);
  29 } /* correct */
  30
  31 void f2(/*@only@*/ st x)
  32 {
  33   free (x);
  34 } /* bad --- didn't release x->b */
  35
  36 void f3(/*@only@*/ st x)
  37 {
  38   free (x->c); /* bad --- x->c is shared */
  39 } /* bad --- didn't release x */
  40
  41 /*@only@*/ st st_create ()
  42 {
  43   st res = (st) smalloc(sizeof(struct _st));
  44   res->a = 3;
  45   return res; /* 6, 7, 8. res->b, res->c, res->d not defined */
  46 }
  47
  48