test/specclauses5.c

   1 /*@-paramuse@*/
   2
   3 typedef struct
   4 {
   5   int id;
   6   char *name;
   7 } *record;
   8
   9 /*@special@*/ record newrecord (void)
  10   /*@defines result@*/
  11   /*@post:isnull result->name@*/
  12 {
  13   record r = (record) malloc (sizeof (*r));
  14
  15   assert (r != NULL);
  16   r->id = 3;
  17   r->name = NULL;
  18   return r;
  19 }
  20
  21 record createrecord (/*@only@*/ char *name)
  22 {
  23   record r = newrecord ();
  24   r->name = name;
  25   return r;
  26 }
  27
  28 record createrecord2 (void)
  29 {
  30   record r = newrecord ();
  31   return r; /* 1. Null storage r->name derivable from return value: r */
  32 }
  33
  34 /*@special@*/ record newrecord2 (void)
  35   /*@defines *result@*/
  36   /*@post:observer result->name@*/
  37 {
  38   record r = (record) malloc (sizeof (*r));
  39
  40   assert (r != NULL);
  41   r->id = 3;
  42   r->name = NULL;
  43   return r; /* 2. Non-observer storage r->name corresponds to storage ... */
  44 }
  45
  46 record createrecordx (void)
  47 {
  48   record r = newrecord2 ();
  49   return r; /* 3. Observer storage r->name reachable from observer return */
  50 }
  51
  52