]>
Commit | Line | Data |
---|---|---|
885824d3 | 1 | # include "bool.h" |
2 | ||
3 | typedef /*@null@*/ int *nip; | |
4 | /*@only@*/ nip gnip; | |
5 | /*@only@*/ int *gip; | |
6 | ||
7 | void g(int *y); | |
8 | ||
9 | /*@truenull@*/ bool ptrpred (nip x) | |
10 | { | |
11 | return (x == NULL); | |
12 | } | |
13 | ||
14 | void f3 (/*@only@*/ nip x) | |
15 | { | |
16 | *gnip = 3; /* 1. Possible dereference of null pointer: *gnip */ | |
17 | *gip = 3; /* okay */ | |
18 | ||
19 | if (x) free (x); | |
20 | } | |
21 | ||
22 | /*@only@*/ int *f (nip arg0, nip arg1, nip arg2, /*@only@*/ int *aip) | |
23 | { | |
24 | int *y = (int *) malloc (sizeof (int)); | |
25 | int *z = (int *) malloc (sizeof (int)); | |
26 | ||
27 | *arg0 = 3; /* 2. Possible dereference of null pointer: *arg0 */ | |
28 | ||
29 | if (arg1) | |
30 | { | |
31 | *arg1 = 7; /* okay */ | |
32 | } | |
33 | else | |
34 | { | |
35 | free (y); /* 3. Possibly null storage passed as non-null param: y */ | |
36 | ||
37 | *z = 3; /* 4. Possible dereference of null pointer: *z */ | |
38 | return z; /* 5. Only storage not released before return: aip */ | |
39 | } | |
40 | ||
41 | /* arg1 is guarded */ | |
42 | ||
43 | *arg1 = 3; /* okay */ | |
44 | *arg2 = 5; /* 6. Possible dereference of null pointer: *arg2 */ | |
45 | *gip = 6; /* okay */ | |
46 | ||
47 | if (z) { *z = 3; } | |
48 | ||
49 | if (gnip) { free (gnip); } else { ; } /* okay */ | |
50 | ||
51 | gnip = z; /* okay */ | |
52 | *gnip = 3; /* 7. Possible dereference of null pointer: *gnip */ | |
53 | gip = z; /* 8, 9. uses z after release, only z not released */ | |
54 | /* Note: gip is possibly null now +++ kept*/ | |
55 | gnip = aip; /* 10. Only storage gnip not released before assignment: gnip = aip */ | |
56 | *gnip = 3; /* okay */ | |
57 | ||
58 | if (y) | |
59 | { | |
60 | return y; /* 11, 12. Returned storage y not completely defined, | |
61 | Function returns with non-null global gip referencing null */ | |
62 | } | |
63 | else | |
64 | { | |
65 | return y; /* 13, 14, 15. Possibly null storage returned as non-null: y, | |
66 | Returned storage y not completely defined, | |
67 | Function returns with non-null global gip referencing null */ | |
68 | } | |
69 | } | |
70 | ||
71 | void f2 (void) | |
72 | { | |
73 | *gnip = 3; /* 16. Possible dereference of null pointer: *gnip */ | |
74 | *gip = 3; /* okay */ | |
75 | } | |
76 | ||
77 | ||
78 | ||
79 |