]>
Commit | Line | Data |
---|---|---|
885824d3 | 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 | /*@pre:isnull *name@*/ | |
12 | { | |
13 | **name = 'a'; /* 1. Dereference of null pointer *name: **name */ | |
14 | } | |
15 | ||
16 | void callname (void) | |
17 | { | |
18 | char **s; | |
19 | ||
20 | s = (char **) malloc (sizeof (char *)); | |
21 | assert (s != NULL); | |
22 | *s = (char *) malloc (sizeof (char)); | |
23 | assert (*s != NULL); | |
24 | ||
25 | **s = 'a'; | |
26 | ||
27 | usename (s); /* 2. Non-null storage *s corresponds to storage listed in ... */ | |
28 | free (*s); | |
29 | free (s); | |
30 | } | |
31 | ||
32 | void nullname (/*@special@*/ char **name) | |
33 | /*@post:isnull *name@*/ | |
34 | { | |
35 | *name = NULL; | |
36 | } | |
37 | ||
38 | void nullname2 (/*@special@*/ char **name) | |
39 | /*@post:isnull *name@*/ | |
40 | { | |
41 | ; | |
42 | } /* 3. Non-null storage *name corresponds to storage listed in ... */ | |
43 | ||
44 | ||
45 | ||
46 | ||
47 |