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
)