test/manual/special.c

   1 typedef struct
   2 {
   3   int id;
   4   /*@only@*/ char *name;
   5 } *record;
   6
   7 static /*@special@*/ record record_new (void)
   8   /*@defines result->id@*/
   9 {
  10   record r = (record) malloc (sizeof (*r));
  11
  12   assert (r != NULL);
  13   r->id = 3;
  14   return r;
  15 }
  16
  17 static void record_setName (/*@special@*/ record r, /*@only@*/ char *name)
  18    /*@defines r->name@*/
  19 {
  20   r->name = name;
  21 }
  22
  23 record record_create (/*@only@*/ char *name)
  24 {
  25   record r = record_new ();
  26   record_setName (r, name);
  27   return r;
  28 }
  29
  30 void record_clearName (/*@special@*/ record r)
  31    /*@releases r->name@*/
  32    /*@post:isnull r->name@*/
  33 {
  34   free (r->name);
  35   r->name = NULL;
  36 }
  37
  38 void record_free (/*@only@*/ record r)
  39 {
  40   record_clearName (r);
  41   free (r);
  42 }
  43
  44
  45
  46
  47