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
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
|
[kernel] Parsing share/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing tests/value/alias.i (no preprocessing)
[value] Analyzing a complete application starting at main8
[value] Computing initial state
[value] Initial state computed
[value:initial-state] Values of globals at initialization
NULL[rbits 0 to 2047] ∈ [--..--]
A ∈ {0}
B ∈ {0}
C ∈ {0}
D ∈ {0}
E ∈ {0}
F ∈ {0}
G ∈ {0}
p[0..4] ∈ {0}
q[0] ∈ {1}
[1] ∈ {2}
[2] ∈ {3}
[3] ∈ {4}
[4] ∈ {5}
p2[0..4] ∈ {0}
q2[0] ∈ {1}
[1] ∈ {2}
[2] ∈ {3}
[3] ∈ {4}
[4] ∈ {5}
p3[0..4] ∈ {0}
t ∈ {0}
u ∈ {0}
v ∈ {0}
w ∈ {0}
x ∈ {0}
y ∈ {0}
z ∈ {0}
t2 ∈ {0}
v2 ∈ {0}
PTR1 ∈ {0}
PTR2 ∈ {0}
PTR3 ∈ {0}
PTR4 ∈ {0}
PTR5 ∈ {0}
PTR6 ∈ {0}
c ∈ [--..--]
c1 ∈ [--..--]
c2 ∈ [--..--]
c3 ∈ [--..--]
c4 ∈ [--..--]
e ∈ {0}
g ∈ {0}
h ∈ {0}
i ∈ {0}
tz1 ∈ {0}
tz2 ∈ {0}
tz3 ∈ {0}
tx ∈ {0}
ty ∈ {0}
tz ∈ {0}
U ∈ {0}
char1 ∈ {0}
ll1 ∈ {0}
[value] Recording results for main8
[value] done for function main8
[value] ====== VALUES COMPUTED ======
[value:final-states] Values at end of function main8:
A ∈ {3; 4}
B ∈ {4; 5}
C ∈ {2; 3; 33; 44}
D ∈ {0; 4; 5; 33; 44}
p[0..1] ∈ {0}
[2] ∈ {0; 33}
[3] ∈ {0; 44}
[4] ∈ {0}
q[0] ∈ {1}
[1] ∈ {2}
[2] ∈ {3}
[3] ∈ {4; 33}
[4] ∈ {5; 44}
q2[0] ∈ {1}
[1] ∈ {2; 33}
[2] ∈ {3; 44}
[3] ∈ {4}
[4] ∈ {5}
t ∈ {4; 5; 6}
u ∈ {0; 5}
v ∈ {0; 5; 44}
w ∈ {0; 4}
x ∈ {0; 4; 33}
y ∈ {0; 1}
z ∈ {0; 4; 33}
PTR1 ∈ {{ &p[2] ; &q[3] }}
PTR2 ∈ {{ &p[3] ; &q[4] }}
PTR3 ∈ {{ &p[2] ; &q[3] }}
PTR4 ∈ {{ &q2{[1], [2]} }}
PTR5 ∈ {{ &p{[2], [3]} ; &q{[3], [4]} }}
tz1 ∈ {0; 1}
tz2 ∈ {0; 1}
tz3 ∈ {0; 1}
tx ∈ {2; 3}
ty ∈ {3; 4}
tz ∈ {5; 6}
[from] Computing for function main8
[from] Done for function main8
[from] ====== DEPENDENCIES COMPUTED ======
These dependencies hold at termination for the executions that terminate:
[from] Function main8:
A FROM c1
B FROM c1
C FROM q2[1..2]; c3
D FROM p[2..3]; q[3..4]; c2; c3
p[2..3] FROM c2 (and SELF)
q[3..4] FROM c2 (and SELF)
q2[1..2] FROM c3 (and SELF)
t FROM c1
u FROM p[3]; q[4]; c2
v FROM p[3]; q[4]; c2
w FROM p[2]; q[3]; c2
x FROM p[2]; q[3]; c2
y FROM c1
z FROM p[2]; q[3]; c2
PTR1 FROM c2
PTR2 FROM c2
PTR3 FROM c2
PTR4 FROM c3
PTR5 FROM c2; c3
tz1 FROM c
tz2 FROM c
tz3 FROM c
tx FROM c
ty FROM c
tz FROM c
[from] ====== END OF DEPENDENCIES ======
[inout] Out (internal) for function main8:
A; B; C; D; p[2..3]; q[3..4]; q2[1..2]; t; u; v; w; x; y; z; PTR1;
PTR2; PTR3; PTR4; PTR5; tz1; tz2; tz3; tx; ty; tz
[inout] Inputs for function main8:
A; B; p[2..3]; q[3..4]; q2[1..2]; PTR1; PTR2; PTR3; PTR4; PTR5; c;
c1; c2; c3; tx; ty; tz
|
