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
|
[kernel] Parsing share/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing tests/float/conv.i (no 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
f ∈ {0}
d ∈ {0}
v ∈ [--..--]
[value] computing for function main1 <- main.
Called from tests/float/conv.i:105.
[value] Called Frama_C_show_each({0})
[value] Called Frama_C_show_each({1.40129846432e-45})
[value] Called Frama_C_show_each([1.40129846432e-43 .. 2.40330263757e+12])
tests/float/conv.i:24:[value] warning: assertion got status unknown.
[value] Called Frama_C_show_each({3.40282346639e+38})
tests/float/conv.i:29:[value] assertion got status valid.
tests/float/conv.i:32:[value] warning: non-finite float value. assert \is_finite(*((float *)(&i)));
[value] Called Frama_C_show_each([-3.40282346639e+38 .. 3.40282346639e+38])
[value] Called Frama_C_show_each({-3.40282346639e+38})
tests/float/conv.i:38:[value] assertion got status valid.
tests/float/conv.i:41:[value] warning: non-finite float value. assert \is_finite(*((float *)(&i)));
[value] Called Frama_C_show_each([-3.40282346639e+38 .. 3.40282346639e+38])
[value] Called Frama_C_show_each([0. .. 1.40129846432e-45])
tests/float/conv.i:48:[value] warning: assertion got status unknown.
tests/float/conv.i:49:[value] warning: non-finite float value. assert \is_finite(*((float *)(&i)));
[value] Called Frama_C_show_each([-3.40282346639e+38 .. 3.40282346639e+38])
tests/float/conv.i:52:[value] warning: non-finite float value. assert \is_finite(*((float *)(&i)));
[value] Called Frama_C_show_each([-3.40282346639e+38 .. 3.40282346639e+38])
tests/float/conv.i:55:[value] warning: non-finite float value. assert \is_finite(*((float *)(&ui)));
[value] Called Frama_C_show_each([-3.40282346639e+38 .. 3.40282346639e+38])
[value] Recording results for main1
[value] Done for function main1
[value] computing for function main2 <- main.
Called from tests/float/conv.i:106.
[value] Called Frama_C_show_each({0})
[value] Called Frama_C_show_each({4.94065645841e-324})
[value] Called Frama_C_show_each([4.94065645841e-322 .. 9.22442153475e+159])
[value] Called Frama_C_show_each({1.79769313486e+308})
tests/float/conv.i:74:[value] assertion got status valid.
tests/float/conv.i:77:[value] warning: non-finite double value. assert \is_finite(*((double *)(&i)));
[value] Called Frama_C_show_each([-1.79769313486e+308 .. 1.79769313486e+308])
tests/float/conv.i:80:[value] warning: non-finite double value. assert \is_finite(*((double *)(&i)));
[value] Called Frama_C_show_each([-1.79769313486e+308 .. 1.79769313486e+308])
[value] Called Frama_C_show_each({-1.79769313486e+308})
tests/float/conv.i:85:[value] assertion got status valid.
tests/float/conv.i:88:[value] warning: non-finite double value. assert \is_finite(*((double *)(&i)));
[value] Called Frama_C_show_each([-1.79769313486e+308 .. 1.79769313486e+308])
[value] Called Frama_C_show_each([0. .. 4.94065645841e-324])
tests/float/conv.i:94:[value] warning: assertion got status unknown.
tests/float/conv.i:95:[value] warning: non-finite double value. assert \is_finite(*((double *)(&i)));
[value] Called Frama_C_show_each([-1.79769313486e+308 .. 1.79769313486e+308])
tests/float/conv.i:98:[value] warning: non-finite double value. assert \is_finite(*((double *)(&i)));
[value] Called Frama_C_show_each([-1.79769313486e+308 .. 1.79769313486e+308])
tests/float/conv.i:101:[value] warning: non-finite double value. assert \is_finite(*((double *)(&ui)));
[value] Called Frama_C_show_each([-1.79769313486e+308 .. 1.79769313486e+308])
[value] Recording results for main2
[value] Done for function main2
[value] Recording results for main
[value] done for function main
[value] ====== VALUES COMPUTED ======
[value:final-states] Values at end of function main1:
f ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
i ∈ {0; 0x7FFFFFFF}
ui ∈ {0xFFFFFFFF}
[value:final-states] Values at end of function main2:
d ∈ {-1.79769313486e+308}
i ∈ {-1; 0}
ui ∈ {0xFFFFFFFFFFFFFFFF}
[value:final-states] Values at end of function main:
f ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
d ∈ {-1.79769313486e+308}
[from] Computing for function main1
[from] Done for function main1
[from] Computing for function main2
[from] Done for function main2
[from] Computing for function main
[from] Done for function main
[from] ====== DEPENDENCIES COMPUTED ======
These dependencies hold at termination for the executions that terminate:
[from] Function main1:
f FROM \nothing
[from] Function main2:
d FROM \nothing
[from] Function main:
f FROM \nothing
d FROM \nothing
[from] ====== END OF DEPENDENCIES ======
[inout] Out (internal) for function main1:
f; i; ui
[inout] Inputs for function main1:
f; v
[inout] Out (internal) for function main2:
d; i; ui
[inout] Inputs for function main2:
d; v
[inout] Out (internal) for function main:
f; d
[inout] Inputs for function main:
f; d; v
|
