]>
Commit | Line | Data |
---|---|---|
885824d3 | 1 | # include "bool.h" |
2 | ||
3 | void g(/*@temp@*/ int *y); | |
4 | ||
5 | /*@truenull@*/ bool ptrpred (/*@out@*/ /*@null@*/ int *x) | |
6 | { | |
3e3ec469 | 7 | return (x == NULL); /* new error detected by out undef */ |
885824d3 | 8 | } |
9 | ||
10 | /*@only@*/ int *f(/*@null@*/ int *x) | |
11 | { | |
12 | int *y = (int *)malloc (sizeof (int)); | |
13 | int *z; | |
14 | int *z2; | |
15 | int *z3; | |
16 | int *z4; | |
17 | int *z5; | |
18 | ||
19 | if (!x) { return x; /* 1. Unqualified storage returned as only: x, | |
20 | ** 2. Possibly null storage returned as non-null: x | |
21 | ** 3. Fresh storage y not released before return | |
22 | */ | |
23 | } | |
24 | ||
25 | z = (int *) malloc (sizeof (int)); | |
26 | z2 = (int *)malloc (sizeof (int)); | |
27 | z3 = (int *)malloc (sizeof (int)); | |
28 | ||
29 | *x = 7; | |
30 | ||
31 | *y = 3; /* 4. Possible dereference of null pointer: *y */ | |
32 | free (y); | |
33 | ||
34 | g(z); /* 5. Possibly null storage passed as non-null param: z | |
35 | ** 6. Passed storage z not completely defined (allocated only): z | |
36 | */ | |
37 | if (z) { *z = 3; } /* okay */ | |
38 | ||
39 | if (!z) { *z = 3; } /* 7. Possible dereference of null pointer: *z */ | |
40 | else { *z = 4; } /* okay */ | |
41 | ||
42 | z4 = (int *)malloc (sizeof (int)); | |
43 | if (z4 == NULL) { *z4 = 3; } /* 8. Possible dereference of null pointer: *z4 */ | |
44 | else { free (z4); } /* [ not any more: 12. Clauses exit... ] */ | |
45 | ||
46 | if (!(z2 != NULL)) { *z2 = 3; } /* 9. Possible dereference of null pointer: *z2 */ | |
47 | ||
48 | if (z3 != NULL) { *z3 = 5; /* okay */ } | |
49 | else { *z3 = 3; } /* 10. Possible dereference of null pointer: *z3 */ | |
50 | if (z2) free (z2); | |
51 | z2 = (int *)malloc (sizeof (int)); | |
52 | ||
53 | if (z2 != NULL) { *z2 = 5; } ; | |
54 | ||
55 | *z2 = 7; /* 11. Possible dereference of null pointer: *z2 */ | |
56 | ||
57 | z5 = (int *) malloc (sizeof (int)); | |
58 | ||
59 | if (ptrpred(z5)) { *z5 = 3; } /* 12. Possible dereference of null pointer: *z5 */ | |
60 | if (!ptrpred(z5)) { *z5 = 3; } | |
61 | ||
62 | if (ptrpred(z5)) { *z5 = 3; } | |
63 | else { free (z5); } | |
64 | ||
65 | free (z2); | |
66 | ||
67 | return z; /* 13. Fresh storage z3 not released */ | |
68 | } | |
69 | ||
70 | ||
71 |