test/observer.c

   1 typedef struct
   2 {
   3   /*@only@*/ char *name;
   4   int   val;
   5 } *stx;
   6
   7 /*@only@*/ char *stx_name (stx x)
   8 {
   9   return (x->name); /* 1. Function returns reference to parameter x: (x->name)
  10                     ** [2]. Return value exposes rep of stx: (x->name)
  11                     ** 3. Released storage x->name reachable from parameter
  12                     */
  13 }
  14
  15 /*@observer@*/ char *stx_observeName (stx x)
  16 {
  17   return (x->name);
  18 }
  19
  20 /*@exposed@*/ char *stx_exposeName (stx x)
  21 {
  22   return (x->name); /* okay */
  23 }
  24
  25 char *f (stx x)
  26 {
  27   char *s;
  28
  29   s = stx_name (x);
  30   free (s);  /* okay */
  31
  32   s = stx_observeName (x);
  33   *s = 'x'; /* 4. Modification of observer */
  34   free (s); /* 5. Pass observer as only */
  35
  36   s = stx_exposeName (x);
  37   *s = 'x'; /* okay */
  38   free (s); /* 6. Pass exposed as only */
  39
  40   s = stx_observeName (x);
  41   return s; /* 7. Observer storage s returned without qualification: s
  42             ** 8. Dependent storage s returned as unqualified: s
  43             */
  44 }
  45
  46
  47
  48
  49
  50
  51