]>
Commit | Line | Data |
---|---|---|
885824d3 | 1 | typedef struct { /*@null@*/ /*@only@*/ int *x; } *st; |
2 | ||
3 | void f(/*@only@*/ st x) | |
4 | { | |
5 | if (x->x != NULL) | |
6 | { | |
7 | free (x->x); | |
8 | } ; | |
9 | ||
10 | free (x); | |
11 | } | |
12 | ||
13 | void f2 (/*@only@*/ st x) | |
14 | { | |
15 | if (x->x != NULL) | |
16 | { | |
17 | free (x->x); | |
18 | } | |
19 | else | |
20 | { | |
21 | ; | |
22 | } | |
23 | ||
24 | free (x); | |
25 | } | |
26 | ||
27 | void g (/*@only@*/ st x) | |
28 | { | |
29 | if (x->x == NULL) | |
30 | { | |
31 | } | |
32 | else | |
33 | { | |
34 | free (x->x); | |
35 | } | |
36 | ||
37 | free (x); | |
38 | } | |
39 | ||
40 | void h(/*@only@*/ st x) | |
41 | { | |
42 | if (7 > 3) | |
43 | { | |
44 | if (x->x != NULL) | |
45 | { | |
46 | free (x->x); | |
47 | } | |
48 | } /* 1. Storage x->x is released in one path, but live in another. */ | |
49 | ||
50 | free (x); | |
51 | } | |
52 | ||
53 | void m(/*@only@*/ st x) | |
54 | { | |
55 | if (7 > 3) | |
56 | { | |
57 | } | |
58 | else | |
59 | { | |
60 | free (x->x); /* 2. Possibly null storage passed as non-null param: x->x */ | |
61 | } /* 3. Storage x->x is released in one path, but live in another. */ | |
62 | ||
63 | free (x); | |
64 | } | |
65 | ||
66 | ||
67 | ||
68 | ||
69 |