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
|
[kernel] Parsing tests/float/init_float.i (no preprocessing)
[value] Analyzing an incomplete application starting at main
[value] Computing initial state
[value] Initial state computed
[value:initial-state] Values of globals at initialization
s.y ∈ [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
r ∈ [-1.9999999999999998*2^1023 .. 1.9999999999999998*2^1023]
cv ∈ [-1.9999999999999998*2^1023 .. 1.9999999999999998*2^1023]
un ∈ [-1.9999999999999998*2^1023 .. 1.9999999999999998*2^1023]
zp ∈ [-1.9999999999999998*2^1023 .. 1.9999999999999998*2^1023]
zm ∈ [-1.9999999999999998*2^1023 .. 1.9999999999999998*2^1023]
zs ∈ [-1.9999999999999998*2^1023 .. 1.9999999999999998*2^1023]
l ∈ [--..--]
Ha[0..4] ∈ [-1.9999999999999998*2^1023 .. 1.9999999999999998*2^1023]
THa[0..4] ∈ [-1.9999999999999998*2^1023 .. 1.9999999999999998*2^1023]
tests/float/init_float.i:16:[value] warning: function main: precondition got status unknown.
tests/float/init_float.i:17:[value] warning: function main: precondition got status unknown.
[value] Recording results for main
[value] done for function main
[value] ====== VALUES COMPUTED ======
[value:final-states] Values at end of function main:
s.y ∈ [-0.0000000000000000 .. 0.0000000000000000]
r ∈ [-1000.0000000000000000 .. 1000.0000000000000000]
cv ∈ [1.0000000715686179 .. 1.6096441013214644*2^20]
un ∈ {1.0000000000000000}
zp ∈ {0}
zm ∈ {-0.0000000000000000}
zs ∈ {0}
l ∈ [4500000000000000001..4700000000000000000]
Ha[0] ∈ {1.9999999999999982*2^-2}
[1] ∈ {1.9999999999999991*2^-2}
[2] ∈ {1.0000000000000000*2^-1}
[3] ∈ {1.0000000000000004*2^-1}
[4] ∈ {1.0000000000000008*2^-1}
THa[0] ∈ {1.4999999999999996}
[1] ∈ {1.4999999999999998}
[2] ∈ {1.5000000000000000}
[3] ∈ {1.5000000000000002}
[4] ∈ {1.5000000000000004}
__retres ∈ {1}
|
