]>
Commit | Line | Data |
---|---|---|
885824d3 | 1 | typedef struct |
2 | { | |
3 | char *name; | |
4 | char *id; | |
5 | int year; | |
6 | } record; | |
7 | ||
8 | extern void setName (/*@special@*/ record *r, /*@only@*/ char *name) | |
9 | /*@defines r->name@*/ ; | |
10 | ||
11 | extern /*@observer@*/ char *getName (/*@special@*/ record r) | |
12 | /*@uses r.name@*/ ; | |
13 | ||
14 | extern void freeName (/*@special@*/ record r) | |
15 | /*@releases r.name@*/ ; | |
16 | ||
17 | extern /*@observer@*/ char *f (/*@only@*/ char *name, char *id) | |
18 | { | |
19 | record r; | |
20 | ||
21 | if (0 == 1) | |
22 | { | |
23 | setName (&r, name); | |
24 | return (getName (r)); /* r.name not released */ | |
25 | } | |
26 | else if (1 == 2) | |
27 | { | |
28 | return (getName (r)); /* r.name not defined */ | |
29 | } | |
30 | else if (2 == 3) | |
31 | { | |
32 | r.name = malloc (sizeof (char) * 12); | |
33 | setName (&r, name); /* r.name allocated, memory leak */ | |
34 | return id; /* r.name not released */ | |
35 | } | |
36 | else | |
37 | { | |
38 | setName (&r, name); | |
39 | freeName (r); | |
40 | printf ("%s\n", r.name); /* dead! */ | |
41 | freeName (r); | |
42 | return id; | |
43 | } | |
44 | } | |
45 |