]> andersk Git - splint.git/blame - test/keep.c
noexpand always false.
[splint.git] / test / keep.c
CommitLineData
885824d3 1/*@only@*/ int *oglob;
2/*@keep@*/ int *kglob;
3
4void f1 (/*@keep@*/ int *x)
5{
6 kglob = x;
7 return;
8}
9
10void f2 (/*@keep@*/ int *x)
11{
12 free (x); /* 1. Keep storage passed as only param: x */
13}
14
15int f3 (/*@keep@*/ int *x)
16{
17 int *y = malloc (sizeof (int));
18
19 if (y == NULL) return 3; /* 2. Keep storage not transferred before return: x */
20
21 *y = 3;
22
23 f1 (x);
24 f1 (y);
25
26 return *x;
27}
28
29int f4 (/*@only@*/ int *x)
30{
31 return (f3 (x));
32}
33
34void f5 (/*@unused@*/ /*@keep@*/ int *x)
35{
36 return; /* 3. Keep storage not transferred before return: x */
37}
38
39void f6 (/*@keep@*/ int *x)
40{
41 if (*x > 3)
42 {
43 f2 (x);
44 } /* 4. Variable x is kept in true branch, but live in continuation. */
45
46 f2 (x); /* 5. Kept storage passed as keep: f2 (x) */
47}
48
49/*@null@*/ int *f7 (/*@null@*/ /*@keep@*/ int *x)
50{
51 if (x == NULL)
52 {
53 ;
54 }
55 else
56 {
57 f2 (x);
58 }
59
60 return x; /* 6. Kept storage x returned as implicitly only: x */
61}
62
63
64
65
66
This page took 0.215542 seconds and 5 git commands to generate.