6 static /*@special@*/ record record_new (void)
7 /*@defines result->id@*/
9 record r = (record) malloc (sizeof (*r));
15 static void record_setName (/*@special@*/ record r, /*@only@*/ char *name)
21 record record_create (/*@only@*/ char *name)
23 record r = record_new ();
24 record_setName (r, name);
28 void record_clearName (/*@special@*/ record r)
29 /*@releases r->name@*/
30 /*@ensures isnull r->name@*/
36 void record_free (/*@only@*/ record r)