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
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
|
[kernel] Parsing share/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing tests/value/struct2.i (no preprocessing)
[value] Analyzing a complete application starting at f_precis
[value] Computing initial state
[value] Initial state computed
[value:initial-state] Values of globals at initialization
NULL[rbits 32768 to 65543] ∈ [--..--]
tabst[0..9] ∈ {0}
tabst2[0..9] ∈ {0}
tab_s[0..1] ∈ {0}
tab_s1[0..1] ∈ {0}
tab_s2[0..1] ∈ {0}
tab_s3[0..1] ∈ {0}
tab_s4[0..1] ∈ {0}
s1 ∈ {0}
s2 ∈ {0}
s4 ∈ {0}
s5 ∈ {0}
s6 ∈ {0}
s8 ∈ {0}
s7 ∈ {0}
tabl[0..9] ∈ {0}
tab1[0..1] ∈ {0}
tab2[0..1] ∈ {0}
tab3[0..1] ∈ {0}
tab4[0..1] ∈ {0}
tab5[0..1] ∈ {0}
tab6[0..1] ∈ {0}
p ∈ {0}
p2 ∈ {0}
p3 ∈ {0}
p4 ∈ {0}
p5 ∈ {0}
p6 ∈ {0}
p7 ∈ {0}
q ∈ {0}
r ∈ {0}
s ∈ {0}
t ∈ {0}
a ∈ {0}
b ∈ {0}
v ∈ [--..--]
Tab[0..9] ∈ {0}
P ∈ {0}
tests/value/struct2.i:74:[value] warning: accessing out of bounds index. assert 0 ≤ i;
tests/value/struct2.i:74:[value] warning: accessing out of bounds index. assert i < 2;
tests/value/struct2.i:76:[value] warning: accessing out of bounds index. assert 0 ≤ (int)(i + j);
tests/value/struct2.i:76:[value] warning: accessing out of bounds index. assert (int)(i + j) < 2;
tests/value/struct2.i:76:[value] warning: signed overflow. assert i + j ≤ 2147483647;
tests/value/struct2.i:78:[value] warning: accessing out of bounds index. assert tab2[i] < 2;
tests/value/struct2.i:80:[value] warning: accessing out of bounds index. assert tab2[1] < 2;
tests/value/struct2.i:82:[value] warning: accessing out of bounds index. assert 0 ≤ (int)(tab2[i] + j);
tests/value/struct2.i:82:[value] warning: accessing out of bounds index. assert (int)(tab2[i] + j) < 2;
tests/value/struct2.i:99:[value] warning: accessing out of bounds index. assert 0 ≤ (int)(tabl[i] + y);
tests/value/struct2.i:99:[value] warning: accessing out of bounds index. assert (int)(tabl[i] + y) < 2;
tests/value/struct2.i:117:[value] warning: signed overflow. assert -2147483648 ≤ *p + x;
tests/value/struct2.i:117:[value] warning: signed overflow. assert *p + x ≤ 2147483647;
tests/value/struct2.i:124:[value] warning: out of bounds read. assert \valid_read(r);
tests/value/struct2.i:124:[kernel] warning: all target addresses were invalid. This path is assumed to be dead.
tests/value/struct2.i:130:[value] warning: out of bounds read. assert \valid_read(p3 + 2);
tests/value/struct2.i:138:[value] warning: signed overflow. assert *((int *)0x1020) + i ≤ 2147483647;
tests/value/struct2.i:149:[value] warning: out of bounds write. assert \valid(*t + i);
tests/value/struct2.i:185:[value] warning: accessing out of bounds index. assert 0 ≤ (int)(i + j);
tests/value/struct2.i:185:[value] warning: accessing out of bounds index. assert (int)(i + j) < 2;
tests/value/struct2.i:185:[value] warning: accessing out of bounds index. assert 0 ≤ k;
tests/value/struct2.i:185:[value] warning: accessing out of bounds index. assert k < 2;
tests/value/struct2.i:185:[value] warning: accessing out of bounds index. assert 0 ≤ l;
tests/value/struct2.i:185:[value] warning: accessing out of bounds index. assert l < 2;
tests/value/struct2.i:185:[value] warning: accessing out of bounds index. assert 0 ≤ (int)(tab3[l] + m);
tests/value/struct2.i:185:[value] warning: accessing out of bounds index. assert (int)(tab3[l] + m) < 10;
tests/value/struct2.i:185:[value] warning: signed overflow. assert -2147483648 ≤ tab3[l] + m;
tests/value/struct2.i:185:[value] warning: signed overflow. assert tab3[l] + m ≤ 2147483647;
[value] Recording results for f_precis
[value] done for function f_precis
tests/value/struct2.i:124:[value] assertion 'Value,mem_access' got final status invalid.
tests/value/struct2.i:130:[value] assertion 'Value,mem_access' got final status invalid.
[value] ====== VALUES COMPUTED ======
[value:final-states] Values at end of function f_precis:
NULL[rbits 32768 to 32799] ∈ {{ NULL + [--..--] ; (? *)&a }}
[rbits 32800 to 65543] ∈ [--..--]
tab_s[0] ∈ {0}
[1].a ∈ [--..--]
[1]{.d[0..9]; .b; .e[0..9]; .c} ∈ {0}
tab_s1[0..1] ∈ {0}
tab_s2[0].a ∈ [--..--]
{[0]{.d[0..9]; .b; .e[0..9]; .c}; [1]} ∈ {0}
tab_s3[0].a ∈ [--..--]
{[0]{.d[0..9]; .b; .e[0..9]; .c}; [1]} ∈ {0}
tab_s4[0].a ∈ [--..--]
[0]{.d[0..9]; .b; .e[0..9]; .c} ∈ {0}
[1].a ∈ [--..--]
[1]{.d[0..9]; .b; .e[0..9]; .c} ∈ {0}
s1.a ∈ [--..--]
.d[0] ∈ {0}
.d[1] ∈ [--..--]
{.d[2..9]; .b; .e[0..9]} ∈ {0}
.c ∈ {{ &s2 }}
s2{.a; .d[0..1]} ∈ [--..--]
.d[2..9] ∈ {0}
.b.a ∈ [--..--]
.b.b ∈ {{ &a }}
.e[0..9] ∈ {0}
.c ∈ {{ &s2 }}
s4{.a; .d[0..9]; .b} ∈ {0}
.e[0].a ∈ [-128..127]
{.e{[0].b; [1..9]}; .c} ∈ {0}
s8.a ∈ {0}
.b ∈ {{ &a }}
s7 ∈ {0}
tab1[0..1] ∈ {2}
tab2[0] ∈ {0; 2}
[1] ∈ {0}
tab3[0..1] ∈ [--..--]
tab4[0] ∈ {0; 2}
[1] ∈ {0}
tab5[0] ∈ {2}
[1] ∈ {0}
tab6[0..1] ∈ {0; 2}
p ∈ {{ &a }}
p2 ∈ {{ &tab1[2] }}
p3 ∈ {{ &tab1{[0], [1]} }}
p4 ∈ {{ &a }}
p5 ∈ {4096}
p6 ∈ {4112}
p7 ∈ {{ &tab1[3] }}
q ∈ {4096}
r ∈ {0}
s ∈ {4144}
t ∈ {4176}
a ∈ [--..--]
b ∈ {0}
[from] Computing for function f_precis
[from] Done for function f_precis
[from] ====== DEPENDENCIES COMPUTED ======
These dependencies hold at termination for the executions that terminate:
[from] Function f_precis:
NULL{[4096..4099]; [4144..4147]} FROM NULL[4176..4179]; i
{[4100..4111]; [4116..4143]; [4148..8192]}
FROM NULL[4176..4179]; i (and SELF)
[4112..4115] FROM NULL{[4128..4131]; [4176..4179]}; i
tab_s[0] FROM s2
[1].a FROM x
tab_s1{[0].b; [1].b} FROM s8; i (and SELF)
tab_s2[0] FROM s2; s8; tabl[0]; x
tab_s3[0].a FROM tabl[1]; x
tab_s4{[0].a; [1].a} FROM tabl[0..1]; x; i; y (and SELF)
s1{.a; .d[1]} FROM x
{.d[0]; .d[2..9]; .e[0..9]} FROM s2
.b FROM s8
.c FROM \nothing
s2{.a; .b.a} FROM x
.d[0..1] FROM x; i (and SELF)
{.b.b; .c} FROM \nothing
s4.e[0].a
FROM NULL{[4176..4179]; [4192]; [4200]}; tabst[2].a;
tabst2{[0].a; [1].a; [2].a; [3].a; [4].a; [5].a; [6].a; [7].a;
[8].a; [9].a};
s5.e[0].b; tab2[0..1]; tab3[0..1]; i; j; k; l; m
s8.b FROM \nothing
s7 FROM s6.b
tab1[0..1] FROM \nothing
tab2[0..1] FROM i (and SELF)
tab3[0..1] FROM i; j; k (and SELF)
tab4[0] FROM tab2[0..1]; v; i (and SELF)
tab5[0] FROM tab2[1]; i
tab6[0..1] FROM tab2[0..1]; i; j (and SELF)
p FROM \nothing
p2 FROM \nothing
p3 FROM i
p4 FROM \nothing
p5 FROM \nothing
p6 FROM \nothing
p7 FROM \nothing
q FROM \nothing
r FROM \nothing
s FROM \nothing
t FROM \nothing
a FROM x
b FROM v; i (and SELF)
[from] ====== END OF DEPENDENCIES ======
[inout] Out (internal) for function f_precis:
NULL[4096..8192]; tab_s{[0]; [1].a}; tab_s1{[0].b; [1].b}; tab_s2[0];
tab_s3[0].a; tab_s4{[0].a; [1].a}; s1; s2{{.a; .d[0..1]}; .b; .c};
s4.e[0].a; s8.b; s7; tab1[0..1]; tab2[0..1]; tab3[0..1]; tab4[0]; tab5[0];
tab6[0..1]; p; p2; p3; p4; p5; p6; p7; q; r; s; t; a; b
[inout] Inputs for function f_precis:
NULL{[4128..4131]; [4176..4179]; [4192]; [4200]}; tabst[2].a;
tabst2{[0].a; [1].a; [2].a; [3].a; [4].a; [5].a; [6].a; [7].a; [8].a;
[9].a}; s1; s2; s5.e[0].b; s6.b; s8; tabl[0..1]; tab1[0..1];
tab2[0..1]; tab3[0..1]; p; p2; p3; p6; q; r; s; t; a; v
|
