test/repexpose.c

   1 # include "repexpose.h"
   2
   3 abst abst_create (/*@dependent@*/ abst p, /*@only@*/ char *x, int i)
   4 {
   5   abst a = (abst) malloc (sizeof (struct _abst));
   6   abst b = p;
   7
   8   a->name = x;            /* 1. Arrow access from possibly null pointer a */
   9   a->val = i;
  10   a->parent = p;          /* [3. exposes rep] */
  11   a->parent = b;          /* [4. exposes rep through alias] */
  12   a->parent = p->parent;  /* [5, 6. exposes rep] */
  13   a->parent = b->parent;  /* 2. Suspect modification of p->parent through alias a->parent */
  14                           /* [7, 8. exposes rep through alias] 3. modifies p */
  15   b = a;
  16   a->name = *globstring;  /* [9, 10.] exposes rep through global */
  17   b->name = *globstring;  /* ??? NO? 3. Suspect modification of *globstring through alias a->name */
  18                           /* [11, 12.] exposes rep through global and alias */
  19   return a; /* 4. Storage a->name reachable from return value is kept */
  20             /* 5. Returned storage *a contains 1 undefined field: im */
  21             /* 6. Storage *globstring reachable from global is kept */
  22 }
  23
  24 /*@only@*/ char *abst_name (abst a)
  25 {
  26   return a->name;   /* 7. Released storage a->name reachable from parameter */
  27                     /* [15, 16.] reference to parameter, exposes rep */
  28 }
  29
  30 int abst_val (abst a)
  31 {
  32   return a->val;
  33 }
  34
  35 int *abst_aval(abst a)
  36 {
  37   return (&(a->val));  /* 9. [17, 18] reference to parameter, exposes rep */
  38 }
  39
  40 abst abst_parent (abst a)
  41 {
  42   abst b = a;
  43
  44   if (TRUE) return b;     /* [19] reference to parameter a */
  45   else return b->parent;  /* 8. Dependent storage b->parent returned as only */
  46                           /* 9. Only storage a not released before return */
  47 }
  48
  49 /*@dependent@*/ char *immut_name (immut im)
  50 {
  51   return (im->name);  /* 10. Only storage im->name returned as dependent: (im->name) */
  52                       /* [23, 24] exposes rep, reference to parameter */
  53 }
  54
  55 void abst_setIm (abst a, immut im)
  56 {
  57   a->im = im;  /* 11. Suspect modification of a->im: a->im = im */
  58                /* 13. [25] modifies a, NO rep exposure since it is immutable! */
  59 }
  60
  61 immut abst_getIm (abst a)
  62 {
  63   return (a->im); /* NO rep exposure since it is immutable */
  64 }
  65
  66