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
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
|
[kernel] Parsing tests/value/dur.i (no preprocessing)
[eva] Analyzing a complete application starting at F2
[eva] Computing initial state
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
G1 ∈ {0}
G2 ∈ {0}
G3 ∈ [--..--]
G4{.M6; .M7; .M8; .M9; .M10; .M11; .M12; .M13; .M14; .M15; .M16; .M17; .M18; .M19; .M20; .M21; .M22; .M23; .M24; .M25; .M26[0..25]; .M27[0..12]; .M28[0..2]; .M29; .M30; .M31; .M32; .M33; .M34; .M35; .M36; .M37; .M38; .M39; .M40; .M41; .M42; .M43; .M44; .M45; .M46; .M47; .M48; .M49; .M50; .M51; .M52; .M53; .M54; .M55; .M56; .M57; .M58; .M59; .M60; .M61; .M62; .M63; .M64[0..26]; .M65[0..26]; .M66[0..47]; .M67[0..47]; .M68[0..47]; .M69[0..47]; .M70[0..47]; .M71[0..47]; .M72[0..47]; .M73[0..47]; .M74[0..9]} ∈
[-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
G5{.M75; .[bits 16 to 31]} ∈ [--..--]
.M76[0].M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M76[0]{.M2; .M3} ∈ [--..--]
.M76[1].M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M76[1]{.M2; .M3} ∈ [--..--]
.M76[2].M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M76[2]{.M2; .M3} ∈ [--..--]
.M76[3].M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M76[3]{.M2; .M3} ∈ [--..--]
.M76[4].M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M76[4]{.M2; .M3} ∈ [--..--]
.M76[5].M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M76[5]{.M2; .M3} ∈ [--..--]
.M76[6].M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M76[6]{.M2; .M3} ∈ [--..--]
.M76[7].M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M76[7]{.M2; .M3} ∈ [--..--]
.M76[8].M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M76[8]{.M2; .M3} ∈ [--..--]
.M76[9].M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M76[9]{.M2; .M3} ∈ [--..--]
.M76[10].M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M76[10]{.M2; .M3} ∈ [--..--]
.M76[11].M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M76[11]{.M2; .M3} ∈ [--..--]
.M76[12].M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M76[12]{.M2; .M3} ∈ [--..--]
.M76[13].M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M76[13]{.M2; .M3} ∈ [--..--]
.M76[14].M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M76[14]{.M2; .M3} ∈ [--..--]
.M76[15].M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M76[15]{.M2; .M3} ∈ [--..--]
.M76[16].M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M76[16]{.M2; .M3} ∈ [--..--]
.M76[17].M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M76[17]{.M2; .M3} ∈ [--..--]
.M76[18].M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M76[18]{.M2; .M3} ∈ [--..--]
.M76[19].M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M76[19]{.M2; .M3} ∈ [--..--]
.M76[20].M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M76[20]{.M2; .M3} ∈ [--..--]
.M76[21].M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M76[21]{.M2; .M3} ∈ [--..--]
.M76[22].M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M76[22]{.M2; .M3} ∈ [--..--]
.M76[23].M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M76[23]{.M2; .M3} ∈ [--..--]
.M76[24].M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M76[24]{.M2; .M3} ∈ [--..--]
.M76[25].M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M76[25]{.M2; .M3} ∈ [--..--]
.M76[26].M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M76[26]{.M2; .M3} ∈ [--..--]
.M76[27].M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M76[27]{.M2; .M3} ∈ [--..--]
.M76[28].M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M76[28]{.M2; .M3} ∈ [--..--]
.M76[29].M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M76[29]{.M2; .M3} ∈ [--..--]
.M76[30].M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M76[30]{.M2; .M3} ∈ [--..--]
.M76[31].M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M76[31]{.M2; .M3} ∈ [--..--]
.M76[32].M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M76[32]{.M2; .M3} ∈ [--..--]
.M76[33].M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M76[33]{.M2; .M3} ∈ [--..--]
.M76[34].M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M76[34]{.M2; .M3} ∈ [--..--]
.M76[35].M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M76[35]{.M2; .M3} ∈ [--..--]
.M76[36].M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M76[36]{.M2; .M3} ∈ [--..--]
.M76[37].M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M76[37]{.M2; .M3} ∈ [--..--]
.M76[38].M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M76[38]{.M2; .M3} ∈ [--..--]
.M76[39].M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M76[39]{.M2; .M3} ∈ [--..--]
.M76[40].M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M76[40]{.M2; .M3} ∈ [--..--]
.M76[41].M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M76[41]{.M2; .M3} ∈ [--..--]
.M76[42].M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M76[42]{.M2; .M3} ∈ [--..--]
.M76[43].M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M76[43]{.M2; .M3} ∈ [--..--]
.M76[44].M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M76[44]{.M2; .M3} ∈ [--..--]
.M76[45].M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M76[45]{.M2; .M3} ∈ [--..--]
.M76[46].M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M76[46]{.M2; .M3} ∈ [--..--]
.M76[47].M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M76[47]{.M2; .M3} ∈ [--..--]
.M76[48].M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M76[48]{.M2; .M3} ∈ [--..--]
.M76[49].M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M76[49]{.M2; .M3} ∈ [--..--]
.M76[50].M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M76[50]{.M2; .M3} ∈ [--..--]
.M76[51].M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M76[51]{.M2; .M3} ∈ [--..--]
.M76[52].M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M76[52]{.M2; .M3} ∈ [--..--]
.M77.M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M77{.M2; .M3} ∈ [--..--]
.M78.M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M78{.M2; .M3} ∈ [--..--]
.M79.M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M79{.M2; .M3} ∈ [--..--]
.M80.M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M80{.M2; .M3} ∈ [--..--]
.M81.M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M81{.M2; .M3} ∈ [--..--]
.M82.M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M82{.M2; .M3} ∈ [--..--]
.M83.M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M83{.M2; .M3} ∈ [--..--]
.M84.M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M84{.M2; .M3} ∈ [--..--]
.M85.M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M85{.M2; .M3} ∈ [--..--]
.M86.M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M86{.M2; .M3} ∈ [--..--]
.M87.M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M87{.M2; .M3} ∈ [--..--]
.M88.M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M88{.M2; .M3} ∈ [--..--]
.M89.M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
{.M89{.M2; .M3}; .M90[0..3]; .M91} ∈ [--..--]
.M92[0].M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M92[0]{.M2; .M3} ∈ [--..--]
.M92[1].M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M92[1]{.M2; .M3} ∈ [--..--]
.M92[2].M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M92[2]{.M2; .M3} ∈ [--..--]
.M92[3].M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M92[3]{.M2; .M3} ∈ [--..--]
.M92[4].M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M92[4]{.M2; .M3} ∈ [--..--]
.M92[5].M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
{.M92[5]{.M2; .M3}; .M93[0..4]} ∈ [--..--]
G6 ∈ [--..--]
G7[0..160] ∈ [--..--]
[eva] tests/value/dur.i:167: starting to merge loop iterations
[eva] Recording results for F2
[eva] done for function F2
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function F2:
G5.M75 ∈ [0..255]
.[bits 16 to 31] ∈ [--..--]
.M76[0].M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M76[0]{.M2; .M3} ∈ [--..--]
.M76[1].M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M76[1]{.M2; .M3} ∈ [--..--]
.M76[2].M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M76[2]{.M2; .M3} ∈ [--..--]
.M76[3].M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M76[3]{.M2; .M3} ∈ [--..--]
.M76[4].M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M76[4]{.M2; .M3} ∈ [--..--]
.M76[5].M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M76[5]{.M2; .M3} ∈ [--..--]
.M76[6].M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M76[6]{.M2; .M3} ∈ [--..--]
.M76[7].M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M76[7]{.M2; .M3} ∈ [--..--]
.M76[8].M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M76[8]{.M2; .M3} ∈ [--..--]
.M76[9].M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M76[9]{.M2; .M3} ∈ [--..--]
.M76[10].M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M76[10]{.M2; .M3} ∈ [--..--]
.M76[11].M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M76[11]{.M2; .M3} ∈ [--..--]
.M76[12].M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M76[12]{.M2; .M3} ∈ [--..--]
.M76[13].M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M76[13]{.M2; .M3} ∈ [--..--]
.M76[14].M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M76[14]{.M2; .M3} ∈ [--..--]
.M76[15].M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M76[15]{.M2; .M3} ∈ [--..--]
.M76[16].M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M76[16]{.M2; .M3} ∈ [--..--]
.M76[17].M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M76[17]{.M2; .M3} ∈ [--..--]
.M76[18].M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M76[18]{.M2; .M3} ∈ [--..--]
.M76[19].M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M76[19]{.M2; .M3} ∈ [--..--]
.M76[20].M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M76[20]{.M2; .M3} ∈ [--..--]
.M76[21].M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M76[21]{.M2; .M3} ∈ [--..--]
.M76[22].M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M76[22]{.M2; .M3} ∈ [--..--]
.M76[23].M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M76[23]{.M2; .M3} ∈ [--..--]
.M76[24].M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M76[24]{.M2; .M3} ∈ [--..--]
.M76[25].M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M76[25]{.M2; .M3} ∈ [--..--]
.M76[26].M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M76[26]{.M2; .M3} ∈ [--..--]
.M76[27].M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M76[27]{.M2; .M3} ∈ [--..--]
.M76[28].M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M76[28]{.M2; .M3} ∈ [--..--]
.M76[29].M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M76[29]{.M2; .M3} ∈ [--..--]
.M76[30].M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M76[30]{.M2; .M3} ∈ [--..--]
.M76[31].M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M76[31]{.M2; .M3} ∈ [--..--]
.M76[32].M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M76[32]{.M2; .M3} ∈ [--..--]
.M76[33].M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M76[33]{.M2; .M3} ∈ [--..--]
.M76[34].M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M76[34]{.M2; .M3} ∈ [--..--]
.M76[35].M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M76[35]{.M2; .M3} ∈ [--..--]
.M76[36].M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M76[36]{.M2; .M3} ∈ [--..--]
.M76[37].M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M76[37]{.M2; .M3} ∈ [--..--]
.M76[38].M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M76[38]{.M2; .M3} ∈ [--..--]
.M76[39].M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M76[39]{.M2; .M3} ∈ [--..--]
.M76[40].M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M76[40]{.M2; .M3} ∈ [--..--]
.M76[41].M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M76[41]{.M2; .M3} ∈ [--..--]
.M76[42].M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M76[42]{.M2; .M3} ∈ [--..--]
.M76[43].M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M76[43]{.M2; .M3} ∈ [--..--]
.M76[44].M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M76[44]{.M2; .M3} ∈ [--..--]
.M76[45].M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M76[45]{.M2; .M3} ∈ [--..--]
.M76[46].M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M76[46]{.M2; .M3} ∈ [--..--]
.M76[47].M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M76[47]{.M2; .M3} ∈ [--..--]
.M76[48].M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M76[48]{.M2; .M3} ∈ [--..--]
.M76[49].M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M76[49]{.M2; .M3} ∈ [--..--]
.M76[50].M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M76[50]{.M2; .M3} ∈ [--..--]
.M76[51].M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M76[51]{.M2; .M3} ∈ [--..--]
.M76[52].M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M76[52]{.M2; .M3} ∈ [--..--]
.M77.M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M77{.M2; .M3} ∈ [--..--]
.M78.M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M78{.M2; .M3} ∈ [--..--]
.M79.M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M79{.M2; .M3} ∈ [--..--]
.M80.M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M80{.M2; .M3} ∈ [--..--]
.M81.M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M81{.M2; .M3} ∈ [--..--]
.M82.M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M82{.M2; .M3} ∈ [--..--]
.M83.M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M83{.M2; .M3} ∈ [--..--]
.M84.M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M84{.M2; .M3} ∈ [--..--]
.M85.M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M85{.M2; .M3} ∈ [--..--]
.M86.M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M86{.M2; .M3} ∈ [--..--]
.M87.M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M87{.M2; .M3} ∈ [--..--]
.M88.M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M88{.M2; .M3} ∈ [--..--]
.M89.M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
{.M89{.M2; .M3}; .M90[0..3]; .M91} ∈ [--..--]
.M92[0].M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M92[0]{.M2; .M3} ∈ [--..--]
.M92[1].M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M92[1]{.M2; .M3} ∈ [--..--]
.M92[2].M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M92[2]{.M2; .M3} ∈ [--..--]
.M92[3].M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M92[3]{.M2; .M3} ∈ [--..--]
.M92[4].M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
.M92[4]{.M2; .M3} ∈ [--..--]
.M92[5].M1 ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
{.M92[5]{.M2; .M3}; .M93[0..4]} ∈ [--..--]
V5 ∈ {4} or UNINITIALIZED
V6 ∈ [--..--] or UNINITIALIZED
V7 ∈ [0..65532],0%2 or UNINITIALIZED
[from] Computing for function F2
[from] Done for function F2
[from] ====== DEPENDENCIES COMPUTED ======
These dependencies hold at termination for the executions that terminate:
[from] Function F2:
G5.M75 FROM G3
{.M90[0].M4; .M90[1].M4; .M90[2].M4; .M90[3].M4}
FROM G1; G2; V8 (and SELF)
{.M90[0].M5; .M90[1].M5; .M90[2].M5; .M90[3].M5} FROM G2; V8 (and SELF)
.M91.M4 FROM G6{.M96[0]; .M97[0]}; V8 (and SELF)
.M91.M5 FROM G6.M97[0]; V8 (and SELF)
[from] ====== END OF DEPENDENCIES ======
[inout] Out (internal) for function F2:
G5{.M75; {.M90[0..3]; .M91}}; V5; V6; V7
[inout] Inputs for function F2:
G1; G2; G3; G5{.M90[0].M4; .M90[1].M4; .M90[2].M4; .M90[3].M4};
G6{.M96[0]; .M97[0]}
|
