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
|
[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:149:[value] function Frama_C_float_interval: precondition got status valid.
share/libc/__fc_builtin.h:150:[value] function Frama_C_float_interval: precondition got status valid.
[value] Done for function Frama_C_float_interval
tests/float/precise_cos_sin.c:15:[kernel] warning: Neither code nor specification for function Frama_C_sin, generating default assigns from the prototype
tests/float/precise_cos_sin.c:15:[value] Frama_C_show_each_s: [-1.6214298009872436*2^-3 .. 1.4685190916061401*2^-5]
tests/float/precise_cos_sin.c:16:[kernel] warning: Neither code nor specification for function Frama_C_cos, generating default assigns from the prototype
tests/float/precise_cos_sin.c:16:[value] Frama_C_show_each_c: [-1.0000000000000000 .. -1.9584906101226807*2^-1]
tests/float/precise_cos_sin.c:15:[value] Frama_C_show_each_s: [-1.7545883655548095*2^-2 .. -1.6214298009872436*2^-3]
tests/float/precise_cos_sin.c:16:[value] Frama_C_show_each_c: [-1.9584906101226807*2^-1 .. -1.7973188161849975*2^-1]
tests/float/precise_cos_sin.c:15:[value] Frama_C_show_each_s: [-1.2946850061416626*2^-1 .. -1.7545883655548095*2^-2]
tests/float/precise_cos_sin.c:16:[value] Frama_C_show_each_c: [-1.7973188161849975*2^-1 .. -1.5243984460830688*2^-1]
tests/float/precise_cos_sin.c:15:[value] Frama_C_show_each_s: [-1.6315786838531494*2^-1 .. -1.2946850061416626*2^-1]
tests/float/precise_cos_sin.c:16:[value] Frama_C_show_each_c: [-1.5243984460830688*2^-1 .. -1.1566983461380005*2^-1]
tests/float/precise_cos_sin.c:15:[value] Frama_C_show_each_s: [-1.8670285940170288*2^-1 .. -1.6315786838531494*2^-1]
tests/float/precise_cos_sin.c:16:[value] Frama_C_show_each_c: [-1.1566983461380005*2^-1 .. -1.4341608285903930*2^-2]
tests/float/precise_cos_sin.c:15:[value] Frama_C_show_each_s: [-1.9863957166671753*2^-1 .. -1.8670285940170288*2^-1]
tests/float/precise_cos_sin.c:16:[value] Frama_C_show_each_c: [-1.4341608285903930*2^-2 .. -1.8630230426788330*2^-4]
tests/float/precise_cos_sin.c:15:[value] Frama_C_show_each_s: [-1.0000000000000000 .. -1.9822584390640259*2^-1]
tests/float/precise_cos_sin.c:16:[value] Frama_C_show_each_c: [-1.8630230426788330*2^-4 .. 1.0632156133651733*2^-3]
tests/float/precise_cos_sin.c:15:[value] Frama_C_show_each_s: [-1.9822584390640259*2^-1 .. -1.8548737764358520*2^-1]
tests/float/precise_cos_sin.c:16:[value] Frama_C_show_each_c: [1.0632156133651733*2^-3 .. 1.4959185123443604*2^-2]
tests/float/precise_cos_sin.c:15:[value] Frama_C_show_each_s: [-1.8548737764358520*2^-1 .. -1.6121622323989868*2^-1]
tests/float/precise_cos_sin.c:16:[value] Frama_C_show_each_c: [1.4959185123443604*2^-2 .. 1.1836102008819580*2^-1]
tests/float/precise_cos_sin.c:15:[value] Frama_C_show_each_s: [-1.6121622323989868*2^-1 .. -1.2692141532897949*2^-1]
tests/float/precise_cos_sin.c:16:[value] Frama_C_show_each_c: [1.1836102008819580*2^-1 .. 1.5456699132919311*2^-1]
tests/float/precise_cos_sin.c:15:[value] Frama_C_show_each_s: [-1.2692141532897949*2^-1 .. -1.6947050094604492*2^-2]
tests/float/precise_cos_sin.c:16:[value] Frama_C_show_each_c: [1.5456699132919311*2^-1 .. 1.8116273880004883*2^-1]
tests/float/precise_cos_sin.c:15:[value] Frama_C_show_each_s: [-1.6947050094604492*2^-2 .. -1.4912263154983521*2^-3]
tests/float/precise_cos_sin.c:16:[value] Frama_C_show_each_c: [1.8116273880004883*2^-1 .. 1.9649466276168823*2^-1]
tests/float/precise_cos_sin.c:15:[value] Frama_C_show_each_s: [-1.4912263154983521*2^-3 .. 1.9986981153488159*2^-5]
tests/float/precise_cos_sin.c:16:[value] Frama_C_show_each_c: [1.9649466276168823*2^-1 .. 1.0000000000000000]
tests/float/precise_cos_sin.c:15:[value] Frama_C_show_each_s: [1.9986981153488159*2^-5 .. 1.2297540903091430*2^-2]
tests/float/precise_cos_sin.c:16:[value] Frama_C_show_each_c: [1.9031358957290649*2^-1 .. 1.9960950613021851*2^-1]
tests/float/precise_cos_sin.c:15:[value] Frama_C_show_each_s: [1.2297540903091430*2^-2 .. 1.0666053295135498*2^-1]
tests/float/precise_cos_sin.c:16:[value] Frama_C_show_each_c: [1.6918489933013916*2^-1 .. 1.9031358957290649*2^-1]
tests/float/precise_cos_sin.c:15:[value] Frama_C_show_each_s: [1.0666053295135498*2^-1 .. 1.4520173072814941*2^-1]
tests/float/precise_cos_sin.c:16:[value] Frama_C_show_each_c: [1.3753710985183716*2^-1 .. 1.6918489933013916*2^-1]
tests/float/precise_cos_sin.c:15:[value] Frama_C_show_each_s: [1.4520173072814941*2^-1 .. 1.7471498250961303*2^-1]
tests/float/precise_cos_sin.c:16:[value] Frama_C_show_each_c: [1.9467586278915405*2^-2 .. 1.3753710985183716*2^-1]
tests/float/precise_cos_sin.c:15:[value] Frama_C_show_each_s: [1.7471498250961303*2^-1 .. 1.9336531162261963*2^-1]
tests/float/precise_cos_sin.c:16:[value] Frama_C_show_each_c: [1.0217350721359252*2^-2 .. 1.9467586278915405*2^-2]
tests/float/precise_cos_sin.c:15:[value] Frama_C_show_each_s: [1.9336531162261963*2^-1 .. 1.9999312162399292*2^-1]
tests/float/precise_cos_sin.c:16:[value] Frama_C_show_each_c: [1.0619176626205444*2^-7 .. 1.0217350721359252*2^-2]
tests/float/precise_cos_sin.c:15:[value] Frama_C_show_each_s: [1.9418631792068481*2^-1 .. 1.0000000000000000]
tests/float/precise_cos_sin.c:16:[value] Frama_C_show_each_c: [-1.9148570299148559*2^-3 .. 1.0619176626205444*2^-7]
tests/float/precise_cos_sin.c:15:[value] Frama_C_show_each_s: [1.7630596160888672*2^-1 .. 1.9418631792068481*2^-1]
tests/float/precise_cos_sin.c:16:[value] Frama_C_show_each_c: [-1.8885136842727661*2^-2 .. -1.9148570299148559*2^-3]
tests/float/precise_cos_sin.c:15:[value] Frama_C_show_each_s: [1.4746373891830444*2^-1 .. 1.7630596160888672*2^-1]
tests/float/precise_cos_sin.c:16:[value] Frama_C_show_each_c: [-1.3510900735855102*2^-1 .. -1.8885136842727661*2^-2]
tests/float/precise_cos_sin.c:15:[value] Frama_C_show_each_s: [1.0945295095443725*2^-1 .. 1.4746373891830444*2^-1]
tests/float/precise_cos_sin.c:16:[value] Frama_C_show_each_c: [-1.6739190816879272*2^-1 .. -1.3510900735855102*2^-1]
tests/float/precise_cos_sin.c:15:[value] Frama_C_show_each_s: [1.2927380800247192*2^-2 .. 1.0945295095443725*2^-1]
tests/float/precise_cos_sin.c:16:[value] Frama_C_show_each_c: [-1.8926719427108764*2^-1 .. -1.6739190816879272*2^-1]
tests/float/precise_cos_sin.c:15:[value] Frama_C_show_each_s: [1.2641634941101074*2^-4 .. 1.2927380800247192*2^-2]
tests/float/precise_cos_sin.c:16:[value] Frama_C_show_each_c: [-1.9937475919723511*2^-1 .. -1.8926719427108764*2^-1]
tests/float/precise_cos_sin.c:15:[value] Frama_C_show_each_s: [-1.4685190916061401*2^-5 .. 1.2641634941101074*2^-4]
tests/float/precise_cos_sin.c:16:[value] Frama_C_show_each_c: [-1.0000000000000000 .. -1.9937475919723511*2^-1]
[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 ∈ [--..--]
f ∈ [3.1875002384185791 .. 3.4375000000000000]
__retres ∈ {0}
|
