]>
Commit | Line | Data |
---|---|---|
885824d3 | 1 | extern /*@only@*/ int *g(/*@only@*/ int *y); |
2 | ||
3 | /*@null@*/ /*@only@*/ int *f(/*@only@*/ int *x) | |
4 | { | |
5 | switch (*x) | |
6 | { | |
7 | case 1: | |
8 | return g(x); | |
9 | case 2: | |
10 | return g(x); | |
11 | case 3: | |
12 | return g(x); | |
13 | default: | |
14 | return g(x); | |
15 | } | |
16 | } | |
17 | ||
18 | /*@null@*/ /*@only@*/ int *f2(/*@only@*/ int *x) | |
19 | { | |
20 | switch (*x) | |
21 | { | |
22 | case 1: | |
23 | return g(x); | |
24 | case 2: | |
25 | return g(x); | |
26 | } /* 1. Variable x is released in one possible execution, but live ... */ | |
27 | ||
28 | return g(x); | |
29 | } | |
30 | ||
31 | /*@null@*/ /*@only@*/ int *f3(/*@only@*/ int *x) | |
32 | { | |
33 | switch (*x) | |
34 | { | |
35 | case 1: | |
36 | return g(x); | |
37 | } | |
38 | ||
39 | return g(x); | |
40 | } |