]>
Commit | Line | Data |
---|---|---|
885824d3 | 1 | # include "bool.h" |
2 | ||
3 | /*@only@*/ /*@null@*/ int *p; | |
4 | ||
5 | extern /*@truenull@*/ bool isNull (/*@null@*/ int *p); | |
6 | ||
7 | void f (void) | |
8 | { | |
9 | if (p != NULL) return; | |
10 | else | |
11 | { | |
12 | p = malloc (24); | |
13 | if (p == NULL) exit (EXIT_FAILURE); | |
14 | *p = 3; | |
15 | } | |
16 | } | |
17 | ||
18 | void f1 (void) | |
19 | { | |
20 | if (p != NULL) return; | |
21 | ||
22 | p = malloc (24); | |
23 | if (p == NULL) exit (EXIT_FAILURE); | |
24 | *p = 3; | |
25 | } | |
26 | ||
27 | int f2 (void) | |
28 | { | |
29 | if (p == NULL) return 0; | |
30 | return *p; | |
31 | } | |
32 | ||
33 | int f3 (void) | |
34 | { | |
35 | if (isNull(p)) return 0; | |
36 | return *p; | |
37 | } | |
38 | ||
39 | void g (void) | |
40 | { | |
41 | if (p == NULL) return; | |
42 | ||
43 | p = malloc (24); /* 1. Only storage p not released before assignment */ | |
44 | if (p == NULL) exit (EXIT_FAILURE); | |
45 | *p = 3; | |
46 | } | |
47 |