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
|
[kernel] Parsing share/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing tests/float/precise_cos_sin.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
Frama_C_entropy_source ∈ [--..--]
[value] computing for function Frama_C_float_interval <- main.
Called from tests/float/precise_cos_sin.c:12.
[value] using specification for function Frama_C_float_interval
share/libc/__fc_builtin.h:141:[value] function Frama_C_float_interval: precondition got status valid.
share/libc/__fc_builtin.h:142:[value] function Frama_C_float_interval: precondition got status valid.
[value] Done for function Frama_C_float_interval
[value] Called Frama_C_show_each_s([-1.6214298009872436*2^-3 .. 1.4685190916061401*2^-5])
[value] Called Frama_C_show_each_c([-1.0000000000000000 .. -1.9584906101226807*2^-1])
[value] Called Frama_C_show_each_s([-1.7545883655548095*2^-2 .. -1.6214298009872436*2^-3])
[value] Called Frama_C_show_each_c([-1.9584906101226807*2^-1 .. -1.7973188161849975*2^-1])
[value] Called Frama_C_show_each_s([-1.2946850061416626*2^-1 .. -1.7545883655548095*2^-2])
[value] Called Frama_C_show_each_c([-1.7973188161849975*2^-1 .. -1.5243984460830688*2^-1])
[value] Called Frama_C_show_each_s([-1.6315786838531494*2^-1 .. -1.2946850061416626*2^-1])
[value] Called Frama_C_show_each_c([-1.5243984460830688*2^-1 .. -1.1566983461380005*2^-1])
[value] Called Frama_C_show_each_s([-1.8670285940170288*2^-1 .. -1.6315786838531494*2^-1])
[value] Called Frama_C_show_each_c([-1.1566983461380005*2^-1 .. -1.4341608285903930*2^-2])
[value] Called Frama_C_show_each_s([-1.9863957166671753*2^-1 .. -1.8670285940170288*2^-1])
[value] Called Frama_C_show_each_c([-1.4341608285903930*2^-2 .. -1.8630230426788330*2^-4])
[value] Called Frama_C_show_each_s([-1.0000000000000000 .. -1.9822584390640259*2^-1])
[value] Called Frama_C_show_each_c([-1.8630230426788330*2^-4 .. 1.0632156133651733*2^-3])
[value] Called Frama_C_show_each_s([-1.9822584390640259*2^-1 .. -1.8548737764358520*2^-1])
[value] Called Frama_C_show_each_c([1.0632156133651733*2^-3 .. 1.4959185123443604*2^-2])
[value] Called Frama_C_show_each_s([-1.8548737764358520*2^-1 .. -1.6121622323989868*2^-1])
[value] Called Frama_C_show_each_c([1.4959185123443604*2^-2 .. 1.1836102008819580*2^-1])
[value] Called Frama_C_show_each_s([-1.6121622323989868*2^-1 .. -1.2692141532897949*2^-1])
[value] Called Frama_C_show_each_c([1.1836102008819580*2^-1 .. 1.5456699132919311*2^-1])
[value] Called Frama_C_show_each_s([-1.2692141532897949*2^-1 .. -1.6947050094604492*2^-2])
[value] Called Frama_C_show_each_c([1.5456699132919311*2^-1 .. 1.8116273880004883*2^-1])
[value] Called Frama_C_show_each_s([-1.6947050094604492*2^-2 .. -1.4912263154983521*2^-3])
[value] Called Frama_C_show_each_c([1.8116273880004883*2^-1 .. 1.9649466276168823*2^-1])
[value] Called Frama_C_show_each_s([-1.4912263154983521*2^-3 .. 1.9986981153488159*2^-5])
[value] Called Frama_C_show_each_c([1.9649466276168823*2^-1 .. 1.0000000000000000])
[value] Called Frama_C_show_each_s([1.9986981153488159*2^-5 .. 1.2297540903091430*2^-2])
[value] Called Frama_C_show_each_c([1.9031358957290649*2^-1 .. 1.9960950613021851*2^-1])
[value] Called Frama_C_show_each_s([1.2297540903091430*2^-2 .. 1.0666053295135498*2^-1])
[value] Called Frama_C_show_each_c([1.6918489933013916*2^-1 .. 1.9031358957290649*2^-1])
[value] Called Frama_C_show_each_s([1.0666053295135498*2^-1 .. 1.4520173072814941*2^-1])
[value] Called Frama_C_show_each_c([1.3753710985183716*2^-1 .. 1.6918489933013916*2^-1])
[value] Called Frama_C_show_each_s([1.4520173072814941*2^-1 .. 1.7471498250961303*2^-1])
[value] Called Frama_C_show_each_c([1.9467586278915405*2^-2 .. 1.3753710985183716*2^-1])
[value] Called Frama_C_show_each_s([1.7471498250961303*2^-1 .. 1.9336531162261963*2^-1])
[value] Called Frama_C_show_each_c([1.0217350721359252*2^-2 .. 1.9467586278915405*2^-2])
[value] Called Frama_C_show_each_s([1.9336531162261963*2^-1 .. 1.9999312162399292*2^-1])
[value] Called Frama_C_show_each_c([1.0619176626205444*2^-7 .. 1.0217350721359252*2^-2])
[value] Called Frama_C_show_each_s([1.9418631792068481*2^-1 .. 1.0000000000000000])
[value] Called Frama_C_show_each_c([-1.9148570299148559*2^-3 .. 1.0619176626205444*2^-7])
[value] Called Frama_C_show_each_s([1.7630596160888672*2^-1 .. 1.9418631792068481*2^-1])
[value] Called Frama_C_show_each_c([-1.8885136842727661*2^-2 .. -1.9148570299148559*2^-3])
[value] Called Frama_C_show_each_s([1.4746373891830444*2^-1 .. 1.7630596160888672*2^-1])
[value] Called Frama_C_show_each_c([-1.3510900735855102*2^-1 .. -1.8885136842727661*2^-2])
[value] Called Frama_C_show_each_s([1.0945295095443725*2^-1 .. 1.4746373891830444*2^-1])
[value] Called Frama_C_show_each_c([-1.6739190816879272*2^-1 .. -1.3510900735855102*2^-1])
[value] Called Frama_C_show_each_s([1.2927380800247192*2^-2 .. 1.0945295095443725*2^-1])
[value] Called Frama_C_show_each_c([-1.8926719427108764*2^-1 .. -1.6739190816879272*2^-1])
[value] Called Frama_C_show_each_s([1.2641634941101074*2^-4 .. 1.2927380800247192*2^-2])
[value] Called Frama_C_show_each_c([-1.9937475919723511*2^-1 .. -1.8926719427108764*2^-1])
[value] Called Frama_C_show_each_s([-1.4685190916061401*2^-5 .. 1.2641634941101074*2^-4])
[value] Called Frama_C_show_each_c([-1.0000000000000000 .. -1.9937475919723511*2^-1])
[value] Recording results for main
[value] done for function main
[value] ====== VALUES COMPUTED ======
|
