10 extern void allocYear (/*@special@*/ record *r)
11 /*@allocates r->year@*/ /* 1. Allocates clause includes *<parameter 1>.year of ... */
14 } /* 2. Unallocated storage r->year corresponds to storage listed ... */
16 extern void setName (/*@special@*/ record *r, /*@only@*/ char *name)
22 extern void setName1 (/*@special@*/ record *r, /*@only@*/ char *name)
26 } /* 3. Storage r->name listed in defines clause not defined at ... */
28 extern void setName2 (/*@special@*/ record *r, char *name)
31 strcpy (r->name, name);
34 extern void setName3 (/*@special@*/ record *r, char *name)
37 } /* 4. Storage *(r->name) listed in sets clause not defined at ... */
39 extern void setName4 (/*@special@*/ record *r, /*@only@*/ char *name)
42 r->name = name; /* 5. Implicitly only storage r->name not released before ... */
45 extern void allocName (/*@special@*/ record *r)
46 /*@allocates r->name@*/
48 r->name = (char *) malloc (sizeof (char) * 20);
51 extern void allocName2 (/*@special@*/ record *r)
52 /*@allocates r->name@*/
54 } /* 6. Storage r->name listed in allocates clauses is not ... */
56 extern void freeName (/*@special@*/ record r)
62 extern void freeName2 (/*@special@*/ record r)
65 } /* 7. Storage r.name listed in releases clause not released */
67 extern void freeName3 (/*@special@*/ record *r)
68 /*@releases r->name@*/
73 extern void freeName4 (/*@special@*/ record *r)
74 /*@releases r->name@*/
76 } /* 8. Storage r->name listed in releases clause not released ... */