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
|
[kernel] Parsing share/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing tests/float/some.c (with preprocessing)
[value] Analyzing a complete application starting at main
[value] Computing initial state
[value] Initial state computed
[value:initial-state] Values of globals at initialization
t[0] ∈ {1.0000000000000000}
[1..54] ∈ {0}
y ∈ {1.0000000000000000*2^-1}
[value] Semantic level unrolling superposing up to 10 states
[value] Semantic level unrolling superposing up to 20 states
[value] Semantic level unrolling superposing up to 30 states
[value] Semantic level unrolling superposing up to 40 states
[value] Semantic level unrolling superposing up to 50 states
[value] DUMPING STATE of file tests/float/some.c line 16
t[0] ∈ {1.0000000000000000}
[1] ∈ {1.5000000000000000}
[2] ∈ {1.7500000000000000}
[3] ∈ {1.8750000000000000}
[4] ∈ {1.9375000000000000}
[5] ∈ {1.9687500000000000}
[6] ∈ {1.9843750000000000}
[7] ∈ {1.9921875000000000}
[8] ∈ {1.9960937500000000}
[9] ∈ {1.9980468750000000}
[10] ∈ {1.9990234375000000}
[11] ∈ {1.9995117187500000}
[12] ∈ {1.9997558593750000}
[13] ∈ {1.9998779296875000}
[14] ∈ {1.9999389648437500}
[15] ∈ {1.9999694824218750}
[16] ∈ {1.9999847412109375}
[17] ∈ {1.9999923706054688}
[18] ∈ {1.9999961853027344}
[19] ∈ {1.9999980926513672}
[20] ∈ {1.9999990463256836}
[21] ∈ {1.9999995231628418}
[22] ∈ {1.9999997615814209}
[23] ∈ {1.9999998807907104}
[24] ∈ {1.9999999403953552}
[25] ∈ {1.9999999701976776}
[26] ∈ {1.9999999850988388}
[27] ∈ {1.9999999925494194}
[28] ∈ {1.9999999962747097}
[29] ∈ {1.9999999981373549}
[30] ∈ {1.9999999990686774}
[31] ∈ {1.9999999995343387}
[32] ∈ {1.9999999997671694}
[33] ∈ {1.9999999998835847}
[34] ∈ {1.9999999999417923}
[35] ∈ {1.9999999999708962}
[36] ∈ {1.9999999999854481}
[37] ∈ {1.9999999999927240}
[38] ∈ {1.9999999999963620}
[39] ∈ {1.9999999999981810}
[40] ∈ {1.9999999999990905}
[41] ∈ {1.9999999999995453}
[42] ∈ {1.9999999999997726}
[43] ∈ {1.9999999999998863}
[44] ∈ {1.9999999999999432}
[45] ∈ {1.9999999999999716}
[46] ∈ {1.9999999999999858}
[47] ∈ {1.9999999999999929}
[48] ∈ {1.9999999999999964}
[49] ∈ {1.9999999999999982}
[50] ∈ {1.9999999999999991}
[51] ∈ {1.9999999999999996}
[52] ∈ {1.9999999999999998}
[53..54] ∈ {2.0000000000000000}
y ∈ {1.0000000000000000*2^-55}
i ∈ {55}
=END OF DUMP==
[value] Recording results for main
[value] done for function main
[value] ====== VALUES COMPUTED ======
|
