3 typedef /*@null@*/ int *mnull;
5 extern /*@notnull@*/ mnull mnull_create (void);
7 extern int f1 (/*@notnull@*/ mnull x); /* 1. Function f1 declared with notnull ... */
11 return *x; /* 2. Possible dereference of null pointer: *x */
14 static /*@unused@*/ int f2 (/*@notnull@*/ mnull x)
19 extern /*@falsenull@*/ bool isThree (mnull x);
21 static /*@unused@*/ int f3 (/*@notnull@*/ mnull x)
23 if (isThree (x)) /* the parameter was missing before 2.4! */
35 /*@notnull@*/ mnull f4 (void)
47 /*@notnull@*/ mnull f5 (void)
49 static /*@only@*/ mnull x = NULL;
59 /*@notnull@*/ mnull f6 (void)
61 static /*@only@*/ mnull x = NULL;
68 return x; /* 3. Possibly null storage returned as non-null */
71 /*@notnull@*/ mnull f7 (void)
73 static /*@only@*/ mnull x = NULL;
84 return x; /* 4. Possibly null storage returned as non-null */