5 /*@truenull@*/ bool ptrpred (/*@out@*/ /*@null@*/ int *x
)
10 /*@only@*/ int *f(/*@null@*/ int *x1
, /*@null@*/ int *x2
,
11 /*@null@*/ int *x3
, /*@null@*/ int *x4
)
15 test
= x1
&& (*x1
== 3); /* okay */
16 test
= !x2
&& (*x2
== 3); /* 1. Possible dereference of null pointer: *x2 */
17 test
= x3
|| (*x3
== 3); /* 2. Possible dereference of null pointer: *x3 */
18 test
= !x4
|| (*x4
== 3); /* okay */
20 test
= ptrpred(x1
) && (*x1
== 3); /* 3. Possible dereference of null pointer: *x1 */
21 test
= !ptrpred(x1
) && (*x1
== 3); /* okay */
28 if (!x4
|| (*x4
== 6))
30 *x4
= 12; /* 4. Possible dereference of null pointer: *x4 */
33 if (!x1
|| (*x1
== 6))
35 return (x3
); /* 5, 6. Unqualified storage returned as only: (x3),
36 Possibly null storage returned as non-null: (x3) */
39 return (x1
); /* 7. Unqualified storage returned as only: (x1)
40 not: null as non-null (because of || semantics) */