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