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
|
[kernel] Parsing share/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing tests/float/absorb.c (with preprocessing)
tests/float/absorb.c:15:[kernel] warning: Floating-point constant 1e-286 is not represented exactly. Will use 0x1.e74404f3daadbp-951. See documentation for option -warn-decimal-float
[value] Analyzing a complete application starting at main
[value] Computing initial state
[value] Initial state computed
[value:initial-state] Values of globals at initialization
Frama_C_entropy_source ∈ [--..--]
x ∈ {0x1.0000000000000p0}
y ∈ {0}
z ∈ {0}
t ∈ {0}
min_f ∈ {0}
min_fl ∈ {0}
den ∈ {0}
[value] computing for function Frama_C_interval <- main.
Called from tests/float/absorb.c:13.
[value] using specification for function Frama_C_interval
share/libc/__fc_builtin.h:50:[value] function Frama_C_interval: precondition got status valid.
[value] Done for function Frama_C_interval
tests/float/absorb.c:16:[value] entering loop for the first time
tests/float/absorb.c:18:[value] warning: non-finite float value.
assert \is_finite((float)((double)((double)x + 1E-286)));
[value] Recording results for main
[value] done for function main
[value] ====== VALUES COMPUTED ======
[value:final-states] Values at end of function main:
Frama_C_entropy_source ∈ [--..--]
x ∈ [0x1.0000000000000p0 .. 0x1.fffffe0000000p127]
y ∈ [0x1.0000000000000p0 .. 0x1.fffffe0000000p127]
z ∈ [0x0.0000000000000p-1022 .. 0x1.0000000000000p-149]
t ∈ [-0x1.bc16d80000000p61 .. 0x1.bc16d80000000p61]
min_f ∈ [0x1.0000000000000p-126 .. 0x1.0000020000000p-126]
min_fl ∈ [-0x1.0000000000000p-126 .. -0x1.fffffc0000000p-127]
den ∈ [0x1.0000000000000p-133 .. 0x1.0001000000000p-133]
b ∈ [-4000000004000000001..4000000004000000001]
[from] Computing for function main
[from] Computing for function Frama_C_interval <-main
[from] Done for function Frama_C_interval
[from] Done for function main
[from] ====== DEPENDENCIES COMPUTED ======
These dependencies hold at termination for the executions that terminate:
[from] Function Frama_C_interval:
Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
\result FROM Frama_C_entropy_source; min; max
[from] Function main:
Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
x FROM x; y (and SELF)
y FROM x; y (and SELF)
z FROM y
t FROM Frama_C_entropy_source
min_f FROM \nothing
min_fl FROM \nothing
den FROM \nothing
[from] ====== END OF DEPENDENCIES ======
[inout] Out (internal) for function main:
Frama_C_entropy_source; x; y; z; t; min_f; min_fl; den; b
[inout] Inputs for function main:
Frama_C_entropy_source; x; y; min_f
|
