test/manual/clauses.c

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