]>
Commit | Line | Data |
---|---|---|
80ee600a | 1 | typedef /*@null@*/ char *ncp; |
2 | ||
3 | void notnullname (ncp *name) | |
4 | /*@ensures notnull *name@*/ | |
5 | { | |
6 | **name = 'a'; /* ensures.c:6:4: Dereference of possibly null pointer *name: **name */ | |
7 | } /* Possibly null storage *name corresponds to storage listed in */ | |
8 | ||
9 | void nullname (/*@unused@*/ char **name) | |
10 | /*@ensures isnull *name@*/ | |
11 | { | |
12 | ; | |
13 | } /* ensures.c:13:2: Non-null storage *name corresponds to storage listed in ensures */ | |
14 | ||
15 | void nullname2 (char **name) | |
16 | /*@ensures isnull *name@*/ | |
17 | { | |
18 | *name = NULL; | |
19 | } | |
20 | ||
21 | void callname (void) | |
22 | { | |
23 | char **s; | |
24 | ||
25 | s = (char **) malloc (sizeof (char *)); | |
26 | assert (s != NULL); | |
27 | *s = NULL; | |
28 | ||
29 | notnullname (s); | |
30 | **s = 'a'; /* okay! */ | |
31 | ||
32 | nullname (s); | |
33 | **s = 'a'; /* ensures.c:33:4: Dereference of null pointer *s: **s */ | |
34 | ||
35 | free (*s); | |
36 | free (s); | |
37 | } | |
38 |