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
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
|
/*@-paramuse@*/
/*@only@*/ int *globonly;
/*@shared@*/ int *globshared1;
/*@shared@*/ int *globshared2;
/*@only@*/ int *zonly;
void f(/*@only@*/ int *x, /*@temp@*/ int *y, /*@shared@*/ int *z)
{
*x = 3;
if (3 > *x)
return; /* 1. bad x not released */
} /* 2. bad x not released */
int f2(/*@temp@*/ int *x, /*@only@*/ int *y)
{
*x = 3;
*y = 6;
return 3; /* 3. bad y not released */
}
void f3(/*@only@*/ int *x)
{
globshared1 = x; /* 4. bad shared globshared1 <- only x */
} /* 5. only not released */
void f4(/*@only@*/ int *x)
{
zonly = x; /* 6. bad - didn't release zonly */
} /* okay */
int g(int *imp)
{
int x = 3;
int *y = malloc(sizeof(int));
int *y2 = malloc(sizeof(int));
int *y3 = malloc(sizeof(int));
if (y2) *y2 = 3;
f3 (imp); /* 7. bad if +memimplicit --- unqualified as only */
*imp = 5; /* 8. uses released */
(void) f(&x, /* 9, 10. pass immediate as only, only parameter aliased */
&x,
globshared1);
(void) f2 (y3, y3); /* 11-15. --- 2 * null passed as nonnull, 2 * not completely def
only parameter y3 aliased */
*y3 = 6; /* 16, 17. bad --- y3 was released, null */
(void) f(y, globshared1, globshared1); /* 18, 19. null as non-null, y not completely def */
(void) f(globshared1, /* 20. pass shared as only */
globshared2,
globshared2);
free (globshared2); /* 21. bad --- free's shared! (pass shared as only) */
free (globonly);
return *y; /* 22-25. y used after release, possible null,
locally allocated y2 not released,
globonly is released */
}
|
