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
|
int *glob;
void stack1 (int **x)
{
int sa[3] = { 0, 1, 2 } ;
int loc = 3;
glob = &loc;
*x = &sa[0];
} /* 1. Stack-allocated storage *x reachable from parameter x,
2. Stack-allocated storage glob reachable from global glob
*/
/*@dependent@*/ int *f (int c)
{
int x = 3;
if (c == 0)
{
return &x; /* 3. Stack-allocated storage &x reachable from return value */
}
else
{
int sa[10];
sa[0] = 35;
sa[2] = 37;
if (c == 1)
{
return sa; /* 4. Stack-allocated storage sa reachable ... */
}
else
{
return &sa[0]; /* 5. Stack-allocated storage sa reachable ... */
}
}
}
|
