]>
Commit | Line | Data |
---|---|---|
885824d3 | 1 | /*@only@*/ int *oglob; |
2 | /*@keep@*/ int *kglob; | |
3 | ||
4 | void f1 (/*@keep@*/ int *x) | |
5 | { | |
6 | kglob = x; | |
7 | return; | |
8 | } | |
9 | ||
10 | void f2 (/*@keep@*/ int *x) | |
11 | { | |
12 | free (x); /* 1. Keep storage passed as only param: x */ | |
13 | } | |
14 | ||
15 | int f3 (/*@keep@*/ int *x) | |
16 | { | |
17 | int *y = malloc (sizeof (int)); | |
18 | ||
19 | if (y == NULL) return 3; /* 2. Keep storage not transferred before return: x */ | |
20 | ||
21 | *y = 3; | |
22 | ||
23 | f1 (x); | |
24 | f1 (y); | |
25 | ||
26 | return *x; | |
27 | } | |
28 | ||
29 | int f4 (/*@only@*/ int *x) | |
30 | { | |
31 | return (f3 (x)); | |
32 | } | |
33 | ||
34 | void f5 (/*@unused@*/ /*@keep@*/ int *x) | |
35 | { | |
36 | return; /* 3. Keep storage not transferred before return: x */ | |
37 | } | |
38 | ||
39 | void f6 (/*@keep@*/ int *x) | |
40 | { | |
41 | if (*x > 3) | |
42 | { | |
43 | f2 (x); | |
44 | } /* 4. Variable x is kept in true branch, but live in continuation. */ | |
45 | ||
46 | f2 (x); /* 5. Kept storage passed as keep: f2 (x) */ | |
47 | } | |
48 | ||
49 | /*@null@*/ int *f7 (/*@null@*/ /*@keep@*/ int *x) | |
50 | { | |
51 | if (x == NULL) | |
52 | { | |
53 | ; | |
54 | } | |
55 | else | |
56 | { | |
57 | f2 (x); | |
58 | } | |
59 | ||
60 | return x; /* 6. Kept storage x returned as implicitly only: x */ | |
61 | } | |
62 | ||
63 | ||
64 | ||
65 | ||
66 |