9 void usename (/*@special@*/ char **name)
11 /*@requires isnull *name@*/
12 /*@ensures notnull *name@*/
14 **name = 'a'; /* 1. Dereference of null pointer *name: **name */
21 s = (char **) malloc (sizeof (char *));
23 *s = (char *) malloc (sizeof (char));
28 usename (s); /* 2. Non-null storage *s corresponds to storage listed in ... */
29 **s = 'a'; /* 3. null! */
34 void nullname (/*@special@*/ char **name)
35 /*@post:isnull *name@*/
40 void nullname2 (/*@special@*/ char **name)
41 /*@post:isnull *name@*/
44 } /* 3. Non-null storage *name corresponds to storage listed in ... */