1 typedef /*@null@*/ char *ncp;
3 void notnullname (ncp *name)
4 /*@ensures notnull *name@*/
6 **name = 'a'; /* ensures.c:6:4: Dereference of possibly null pointer *name: **name */
7 } /* Possibly null storage *name corresponds to storage listed in */
9 void nullname (/*@unused@*/ char **name)
10 /*@ensures isnull *name@*/
13 } /* ensures.c:13:2: Non-null storage *name corresponds to storage listed in ensures */
15 void nullname2 (char **name)
16 /*@ensures isnull *name@*/
25 s = (char **) malloc (sizeof (char *));
30 **s = 'a'; /* okay! */
33 **s = 'a'; /* ensures.c:33:4: Dereference of null pointer *s: **s */