]>
Commit | Line | Data |
---|---|---|
80ee600a | 1 | /*@-paramuse@*/ |
2 | ||
3 | typedef struct | |
4 | { | |
5 | int id; | |
6 | char *name; | |
7 | } *record; | |
8 | ||
9 | void usename (/*@special@*/ char **name) | |
10 | /*@uses *name@*/ | |
11 | /*@requires isnull *name@*/ | |
12 | /*@ensures notnull *name@*/ | |
13 | { | |
14 | **name = 'a'; /* 1. Dereference of null pointer *name: **name */ | |
15 | } | |
16 | ||
17 | void callname (void) | |
18 | { | |
19 | char **s; | |
20 | ||
21 | s = (char **) malloc (sizeof (char *)); | |
22 | assert (s != NULL); | |
23 | *s = (char *) malloc (sizeof (char)); | |
24 | assert (*s != NULL); | |
25 | ||
26 | **s = 'a'; | |
27 | ||
28 | usename (s); /* 2. Non-null storage *s corresponds to storage listed in ... */ | |
29 | **s = 'a'; /* 3. null! */ | |
30 | free (*s); | |
31 | free (s); | |
32 | } | |
33 | ||
34 | void nullname (/*@special@*/ char **name) | |
35 | /*@post:isnull *name@*/ | |
36 | { | |
37 | *name = NULL; | |
38 | } | |
39 | ||
40 | void nullname2 (/*@special@*/ char **name) | |
41 | /*@post:isnull *name@*/ | |
42 | { | |
43 | ; | |
44 | } /* 3. Non-null storage *name corresponds to storage listed in ... */ | |
45 | ||
46 | ||
47 | ||
48 | ||
49 |