]>
Commit | Line | Data |
---|---|---|
885824d3 | 1 | /*@-paramuse@*/ |
2 | ||
3 | typedef struct | |
4 | { | |
5 | char *name; | |
6 | char *id; | |
7 | int year; | |
8 | } record; | |
9 | ||
10 | extern void allocYear (/*@special@*/ record *r) | |
11 | /*@allocates r->year@*/ /* 1. Allocates clause includes *<parameter 1>.year of ... */ | |
12 | { | |
13 | r->year = 23; | |
14 | } /* 2. Unallocated storage r->year corresponds to storage listed ... */ | |
15 | ||
16 | extern void setName (/*@special@*/ record *r, /*@only@*/ char *name) | |
17 | /*@defines r->name@*/ | |
18 | { | |
19 | r->name = name; | |
20 | } | |
21 | ||
22 | extern void setName1 (/*@special@*/ record *r, /*@only@*/ char *name) | |
23 | /*@defines r->name@*/ | |
24 | { | |
25 | free (name); | |
26 | } /* 3. Storage r->name listed in defines clause not defined at ... */ | |
27 | ||
28 | extern void setName2 (/*@special@*/ record *r, char *name) | |
29 | /*@sets r->name@*/ | |
30 | { | |
31 | strcpy (r->name, name); | |
32 | } | |
33 | ||
34 | extern void setName3 (/*@special@*/ record *r, char *name) | |
35 | /*@sets r->name@*/ | |
36 | { | |
37 | } /* 4. Storage *(r->name) listed in sets clause not defined at ... */ | |
38 | ||
39 | extern void setName4 (/*@special@*/ record *r, /*@only@*/ char *name) | |
40 | /*@sets r->name@*/ | |
41 | { | |
42 | r->name = name; /* 5. Implicitly only storage r->name not released before ... */ | |
43 | } | |
44 | ||
45 | extern void allocName (/*@special@*/ record *r) | |
46 | /*@allocates r->name@*/ | |
47 | { | |
48 | r->name = (char *) malloc (sizeof (char) * 20); | |
49 | } | |
50 | ||
51 | extern void allocName2 (/*@special@*/ record *r) | |
52 | /*@allocates r->name@*/ | |
53 | { | |
54 | } /* 6. Storage r->name listed in allocates clauses is not ... */ | |
55 | ||
56 | extern void freeName (/*@special@*/ record r) | |
57 | /*@releases r.name@*/ | |
58 | { | |
59 | free (r.name); | |
60 | } | |
61 | ||
62 | extern void freeName2 (/*@special@*/ record r) | |
63 | /*@releases r.name@*/ | |
64 | { | |
65 | } /* 7. Storage r.name listed in releases clause not released */ | |
66 | ||
67 | extern void freeName3 (/*@special@*/ record *r) | |
68 | /*@releases r->name@*/ | |
69 | { | |
70 | free (r->name); | |
71 | } | |
72 | ||
73 | extern void freeName4 (/*@special@*/ record *r) | |
74 | /*@releases r->name@*/ | |
75 | { | |
76 | } /* 8. Storage r->name listed in releases clause not released ... */ |