Skip to content
Snippets Groups Projects
Commit 9366f3cf authored by David Bühler's avatar David Bühler
Browse files

[Floating_point] Uses exponent p0 when printing ±0. as hexadecimal. 

Instead of p-1022, which was misleading on single precision float.
parent 21cbe17a
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 87 additions and 100 deletions
src/libraries/utils/floating_point.ml
+ 1
− 1
View file @ 9366f3cf
...@@ -295,7 +295,7 @@ let pretty_normal ~use_hex fmt f = ...@@ -295,7 +295,7 @@ let pretty_normal ~use_hex fmt f =
let firstdigit, exp = let firstdigit, exp =
if exp <> 0 if exp <> 0
then 1, (exp - 1023) then 1, (exp - 1023)
else 0, -1022 else 0, if f = 0. then 0 else -1022
in in
if not use_hex if not use_hex
then begin then begin
......
tests/float/oracle/cond.res.oracle
+ 1
− 1
View file @ 9366f3cf
...@@ -40,7 +40,7 @@ ...@@ -40,7 +40,7 @@
[eva] ====== VALUES COMPUTED ====== [eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main: [eva:final-states] Values at end of function main:
Frama_C_entropy_source ∈ [--..--] Frama_C_entropy_source ∈ [--..--]
x ∈ [-0x0.0000000000000p-1022 .. 0x1.4000000000000p3] x ∈ [-0x0.0000000000000p0 .. 0x1.4000000000000p3]
dx ∈ [0x1.0000000000001p0 .. 0x1.4000000000000p3] dx ∈ [0x1.0000000000001p0 .. 0x1.4000000000000p3]
dz ∈ [0x1.0000000000001p0 .. 0x1.4000000000000p3] dz ∈ [0x1.0000000000001p0 .. 0x1.4000000000000p3]
dt ∈ [-0x1.4000000000000p3 .. 0x1.fffffffffffffp-1] dt ∈ [-0x1.4000000000000p3 .. 0x1.fffffffffffffp-1]
......
tests/float/oracle/const.res.oracle
+ 8
− 8
View file @ 9366f3cf
[kernel] Parsing tests/float/const.i (no preprocessing) [kernel] Parsing tests/float/const.i (no preprocessing)
[kernel:parser:decimal-float] tests/float/const.i:21: Warning: [kernel:parser:decimal-float] tests/float/const.i:21: Warning:
Floating-point constant 0.0000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000024703282292062327208828439643411068618252990130716238221279284125033775363510437593264991818081799618989828234772285886546332835517796989819938739800539093906315035659515570226392290858392449105184435931802849936536152500319370457678249219365623669863658480757001585769269903706311928279558551332927834338409351978015531246597263579574622766465272827220056374006485499977096599470454020828166226237857393450736339007967761930577506740176324673600968951340535537458516661134223766678604162159680461914467291840300530057530849048765391711386591646239524912623653881879636239373280423891018672348497668235089863388587925628302755995657524455507255189313690836254779186948667994968324049705821028513185451396213837722826145437693412532098591327667236328125 is not represented exactly. Will use 0x0.0000000000000p-1022. Floating-point constant 0.0000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000024703282292062327208828439643411068618252990130716238221279284125033775363510437593264991818081799618989828234772285886546332835517796989819938739800539093906315035659515570226392290858392449105184435931802849936536152500319370457678249219365623669863658480757001585769269903706311928279558551332927834338409351978015531246597263579574622766465272827220056374006485499977096599470454020828166226237857393450736339007967761930577506740176324673600968951340535537458516661134223766678604162159680461914467291840300530057530849048765391711386591646239524912623653881879636239373280423891018672348497668235089863388587925628302755995657524455507255189313690836254779186948667994968324049705821028513185451396213837722826145437693412532098591327667236328125 is not represented exactly. Will use 0x0.0000000000000p0.
[kernel:parser:decimal-float] tests/float/const.i:22: Warning: [kernel:parser:decimal-float] tests/float/const.i:22: Warning:
Floating-point constant 0.000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000002470328229206232720882843964341106861825299013071623822127928412503377536351043759326499181808179961898982823477228588654633283551779698981993873980053909390631503565951557022639229085839244910518443593180284993653615250031937045767824921936562366986365848075700158576926990370631192827955855133292783433840935197801553124659726357957462276646527282722005637400648549997709659947045402082816622623785739345073633900796776193057750674017632467360096895134053553745851666113422376667860416215968046191446729184030053005753084904876539171138659164623952491262365388187963623937328042389101867234849766823508986338858792562830275599565752445550725518931369083625477918694866799496832404970582102851318545139621383772282614543769341253209859132766723632812501 is not represented exactly. Will use 0x0.0000000000001p-1022. Floating-point constant 0.000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000002470328229206232720882843964341106861825299013071623822127928412503377536351043759326499181808179961898982823477228588654633283551779698981993873980053909390631503565951557022639229085839244910518443593180284993653615250031937045767824921936562366986365848075700158576926990370631192827955855133292783433840935197801553124659726357957462276646527282722005637400648549997709659947045402082816622623785739345073633900796776193057750674017632467360096895134053553745851666113422376667860416215968046191446729184030053005753084904876539171138659164623952491262365388187963623937328042389101867234849766823508986338858792562830275599565752445550725518931369083625477918694866799496832404970582102851318545139621383772282614543769341253209859132766723632812501 is not represented exactly. Will use 0x0.0000000000001p-1022.
[kernel:parser:decimal-float] tests/float/const.i:23: Warning: [kernel:parser:decimal-float] tests/float/const.i:23: Warning:
Floating-point constant 0.000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000002470328229206232720882843964341106861825299013071623822127928412503377536351043759326499181808179961898982823477228588654633283551779698981993873980053909390631503565951557022639229085839244910518443593180284993653615250031937045767824921936562366986365848075700158576926990370631192827955855133292783433840935197801553124659726357957462276646527282722005637400648549997709659947045402082816622623785739345073633900796776193057750674017632467360096895134053553745851666113422376667860416215968046191446729184030053005753084904876539171138659164623952491262365388187963623937328042389101867234849766823508986338858792562830275599565752445550725518931369083625477918694866799496832404970582102851318545139621383772282614543769341253209859132766723632812499 is not represented exactly. Will use 0x0.0000000000000p-1022. Floating-point constant 0.000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000002470328229206232720882843964341106861825299013071623822127928412503377536351043759326499181808179961898982823477228588654633283551779698981993873980053909390631503565951557022639229085839244910518443593180284993653615250031937045767824921936562366986365848075700158576926990370631192827955855133292783433840935197801553124659726357957462276646527282722005637400648549997709659947045402082816622623785739345073633900796776193057750674017632467360096895134053553745851666113422376667860416215968046191446729184030053005753084904876539171138659164623952491262365388187963623937328042389101867234849766823508986338858792562830275599565752445550725518931369083625477918694866799496832404970582102851318545139621383772282614543769341253209859132766723632812499 is not represented exactly. Will use 0x0.0000000000000p0.
[kernel:parser:decimal-float] tests/float/const.i:26: Warning: [kernel:parser:decimal-float] tests/float/const.i:26: Warning:
Floating-point constant 0.0000000000000000000000000000000000000000000014012984643248170709237295832899161312802619418765157717570682838897910826858606014866381883621215820312499 is not represented exactly. Will use 0x1.0000000000000p-149. Floating-point constant 0.0000000000000000000000000000000000000000000014012984643248170709237295832899161312802619418765157717570682838897910826858606014866381883621215820312499 is not represented exactly. Will use 0x1.0000000000000p-149.
[kernel:parser:decimal-float] tests/float/const.i:27: Warning: [kernel:parser:decimal-float] tests/float/const.i:27: Warning:
...@@ -18,9 +18,9 @@ ...@@ -18,9 +18,9 @@
[kernel:parser:decimal-float] tests/float/const.i:34: Warning: [kernel:parser:decimal-float] tests/float/const.i:34: Warning:
Floating-point constant 0.00000000000000000000000000000000000000000000070064923216240853546186479164495806564013097093825788587853414194489554134293030074331909418106079101562501 is not represented exactly. Will use 0x1.0000000000000p-150. Floating-point constant 0.00000000000000000000000000000000000000000000070064923216240853546186479164495806564013097093825788587853414194489554134293030074331909418106079101562501 is not represented exactly. Will use 0x1.0000000000000p-150.
[kernel:parser:decimal-float] tests/float/const.i:35: Warning: [kernel:parser:decimal-float] tests/float/const.i:35: Warning:
Floating-point constant 0.000000000000000000000000000000000000000000000700649232162408535461864791644958065640130970938257885878534141944895541342930300743319094181060791015625f is not represented exactly. Will use 0x0.0000000000000p-1022. Floating-point constant 0.000000000000000000000000000000000000000000000700649232162408535461864791644958065640130970938257885878534141944895541342930300743319094181060791015625f is not represented exactly. Will use 0x0.0000000000000p0.
[kernel:parser:decimal-float] tests/float/const.i:36: Warning: [kernel:parser:decimal-float] tests/float/const.i:36: Warning:
Floating-point constant 0.00000000000000000000000000000000000000000000070064923216240853546186479164495806564013097093825788587853414194489554134293030074331909418106079101562499f is not represented exactly. Will use 0x0.0000000000000p-1022. Floating-point constant 0.00000000000000000000000000000000000000000000070064923216240853546186479164495806564013097093825788587853414194489554134293030074331909418106079101562499f is not represented exactly. Will use 0x0.0000000000000p0.
[kernel:parser:decimal-float] tests/float/const.i:37: Warning: [kernel:parser:decimal-float] tests/float/const.i:37: Warning:
Floating-point constant 0.00000000000000000000000000000000000000000000070064923216240853546186479164495806564013097093825788587853414194489554134293030074331909418106079101562501f is not represented exactly. Will use 0x1.0000000000000p-149. Floating-point constant 0.00000000000000000000000000000000000000000000070064923216240853546186479164495806564013097093825788587853414194489554134293030074331909418106079101562501f is not represented exactly. Will use 0x1.0000000000000p-149.
[eva] Analyzing a complete application starting at main [eva] Analyzing a complete application starting at main
...@@ -137,11 +137,11 @@ ...@@ -137,11 +137,11 @@
[eva] done for function main [eva] done for function main
[eva] ====== VALUES COMPUTED ====== [eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main: [eva:final-states] Values at end of function main:
f_ ∈ {-0x0.0000000000000p-1022} f_ ∈ {-0x0.0000000000000p0}
f00 ∈ {0} f00 ∈ {0}
f2 ∈ {0x1.8000000000000p1} f2 ∈ {0x1.8000000000000p1}
f3 ∈ {0x1.8000000000000p1} f3 ∈ {0x1.8000000000000p1}
f_0 ∈ [-0x0.0000000000000p-1022 .. 0x0.0000000000000p-1022] f_0 ∈ [-0x0.0000000000000p0 .. 0x0.0000000000000p0]
f13 ∈ [0x1.0000000000000p0 .. 0x1.8000000000000p1] f13 ∈ [0x1.0000000000000p0 .. 0x1.8000000000000p1]
f26 ∈ [0x1.0000000000000p1 .. 0x1.8000000000000p2] f26 ∈ [0x1.0000000000000p1 .. 0x1.8000000000000p2]
fic0 ∈ {0} fic0 ∈ {0}
...@@ -151,10 +151,10 @@ ...@@ -151,10 +151,10 @@
fec0 ∈ {0} fec0 ∈ {0}
fec2 ∈ {0x1.0000000000000p1} fec2 ∈ {0x1.0000000000000p1}
fec4 ∈ {0x1.0000000000000p2} fec4 ∈ {0x1.0000000000000p2}
m_ ∈ {-0x0.0000000000000p-1022} m_ ∈ {-0x0.0000000000000p0}
m00 ∈ {0} m00 ∈ {0}
m2 ∈ {0x1.8000000000000p1} m2 ∈ {0x1.8000000000000p1}
m_0 ∈ [-0x0.0000000000000p-1022 .. 0x0.0000000000000p-1022] m_0 ∈ [-0x0.0000000000000p0 .. 0x0.0000000000000p0]
m13 ∈ [0x1.0000000000000p0 .. 0x1.8000000000000p1] m13 ∈ [0x1.0000000000000p0 .. 0x1.8000000000000p1]
m26 ∈ [0x1.0000000000000p1 .. 0x1.8000000000000p2] m26 ∈ [0x1.0000000000000p1 .. 0x1.8000000000000p2]
d2 ∈ {0x1.8000000000000p1} d2 ∈ {0x1.8000000000000p1}
......
tests/float/oracle/logic.0.res.oracle
+ 34
− 43
View file @ 9366f3cf
...@@ -112,55 +112,46 @@ ...@@ -112,55 +112,46 @@
Called from tests/float/logic.i:118. Called from tests/float/logic.i:118.
[eva] tests/float/logic.i:84: [eva] tests/float/logic.i:84:
Frama_C_show_each_eq: Frama_C_show_each_eq:
{-0x0.0000000000000p-1022}, {-0x0.0000000000000p0}, [-0x0.0000000000000p0 .. 0x0.0000000000000p0]
[-0x0.0000000000000p-1022 .. 0x0.0000000000000p-1022]
[eva] tests/float/logic.i:88: [eva] tests/float/logic.i:88:
Frama_C_show_each_lt: Frama_C_show_each_lt:
{-0x0.0000000000000p-1022}, {-0x0.0000000000000p0}, [-0x1.fffffffffffffp1023 .. -0x0.0000000000001p-1022]
[-0x1.fffffffffffffp1023 .. -0x0.0000000000001p-1022]
[eva] tests/float/logic.i:92: [eva] tests/float/logic.i:92:
Frama_C_show_each_lt: Frama_C_show_each_lt:
{-0x0.0000000000000p-1022}, {-0x0.0000000000000p0}, [-0x1.fffffffffffffp1023 .. 0x0.0000000000000p0]
[-0x1.fffffffffffffp1023 .. 0x0.0000000000000p-1022]
[eva] tests/float/logic.i:96: [eva] tests/float/logic.i:96:
Frama_C_show_each_eq_double: Frama_C_show_each_eq_double:
{-0x0.0000000000000p-1022}, {-0x0.0000000000000p0}, [-0x0.0000000000000p0 .. 0x0.0000000000000p0]
[-0x0.0000000000000p-1022 .. 0x0.0000000000000p-1022]
[eva] tests/float/logic.i:100: [eva] tests/float/logic.i:100:
Frama_C_show_each_lt_double: Frama_C_show_each_lt_double:
{-0x0.0000000000000p-1022}, {-0x0.0000000000000p0}, [-0x1.fffffffffffffp1023 .. -0x0.0000000000001p-1022]
[-0x1.fffffffffffffp1023 .. -0x0.0000000000001p-1022]
[eva] tests/float/logic.i:104: [eva] tests/float/logic.i:104:
Frama_C_show_each_le_double: Frama_C_show_each_le_double:
{-0x0.0000000000000p-1022}, {-0x0.0000000000000p0}, [-0x1.fffffffffffffp1023 .. 0x0.0000000000000p0]
[-0x1.fffffffffffffp1023 .. 0x0.0000000000000p-1022]
[eva] tests/float/logic.i:108: [eva] tests/float/logic.i:108:
Frama_C_show_each_ne_double: Frama_C_show_each_ne_double:
{-0x0.0000000000000p-1022}, {-0x0.0000000000000p0}, [-0x1.fffffffffffffp1023 .. 0x1.fffffffffffffp1023]
[-0x1.fffffffffffffp1023 .. 0x1.fffffffffffffp1023]
[eva] Recording results for test_comparison_reduction [eva] Recording results for test_comparison_reduction
[eva] Done for function test_comparison_reduction [eva] Done for function test_comparison_reduction
[eva] computing for function test_comparison_reduction <- [eva] computing for function test_comparison_reduction <-
test_builtin_comparisons <- main. test_builtin_comparisons <- main.
Called from tests/float/logic.i:119. Called from tests/float/logic.i:119.
[eva] tests/float/logic.i:84: [eva] tests/float/logic.i:84:
Frama_C_show_each_eq: Frama_C_show_each_eq: {0}, [-0x0.0000000000000p0 .. 0x0.0000000000000p0]
{0}, [-0x0.0000000000000p-1022 .. 0x0.0000000000000p-1022]
[eva] tests/float/logic.i:88: [eva] tests/float/logic.i:88:
Frama_C_show_each_lt: Frama_C_show_each_lt:
{0}, [-0x1.fffffffffffffp1023 .. -0x0.0000000000001p-1022] {0}, [-0x1.fffffffffffffp1023 .. -0x0.0000000000001p-1022]
[eva] tests/float/logic.i:92: [eva] tests/float/logic.i:92:
Frama_C_show_each_lt: Frama_C_show_each_lt: {0}, [-0x1.fffffffffffffp1023 .. 0x0.0000000000000p0]
{0}, [-0x1.fffffffffffffp1023 .. 0x0.0000000000000p-1022]
[eva] tests/float/logic.i:96: [eva] tests/float/logic.i:96:
Frama_C_show_each_eq_double: Frama_C_show_each_eq_double:
{0}, [-0x0.0000000000000p-1022 .. 0x0.0000000000000p-1022] {0}, [-0x0.0000000000000p0 .. 0x0.0000000000000p0]
[eva] tests/float/logic.i:100: [eva] tests/float/logic.i:100:
Frama_C_show_each_lt_double: Frama_C_show_each_lt_double:
{0}, [-0x1.fffffffffffffp1023 .. -0x0.0000000000001p-1022] {0}, [-0x1.fffffffffffffp1023 .. -0x0.0000000000001p-1022]
[eva] tests/float/logic.i:104: [eva] tests/float/logic.i:104:
Frama_C_show_each_le_double: Frama_C_show_each_le_double:
{0}, [-0x1.fffffffffffffp1023 .. 0x0.0000000000000p-1022] {0}, [-0x1.fffffffffffffp1023 .. 0x0.0000000000000p0]
[eva] tests/float/logic.i:108: [eva] tests/float/logic.i:108:
Frama_C_show_each_ne_double: Frama_C_show_each_ne_double:
{0}, [-0x1.fffffffffffffp1023 .. 0x1.fffffffffffffp1023] {0}, [-0x1.fffffffffffffp1023 .. 0x1.fffffffffffffp1023]
...@@ -228,31 +219,31 @@ ...@@ -228,31 +219,31 @@
Called from tests/float/logic.i:126. Called from tests/float/logic.i:126.
[eva] tests/float/logic.i:84: [eva] tests/float/logic.i:84:
Frama_C_show_each_eq: Frama_C_show_each_eq:
[-0x1.4000000000000p3 .. -0x0.0000000000000p-1022], [-0x1.4000000000000p3 .. -0x0.0000000000000p0],
[-0x1.4000000000000p3 .. 0x0.0000000000000p-1022] [-0x1.4000000000000p3 .. 0x0.0000000000000p0]
[eva] tests/float/logic.i:88: [eva] tests/float/logic.i:88:
Frama_C_show_each_lt: Frama_C_show_each_lt:
[-0x1.4000000000000p3 .. -0x0.0000000000000p-1022], [-0x1.4000000000000p3 .. -0x0.0000000000000p0],
[-0x1.fffffffffffffp1023 .. -0x0.0000000000001p-1022] [-0x1.fffffffffffffp1023 .. -0x0.0000000000001p-1022]
[eva] tests/float/logic.i:92: [eva] tests/float/logic.i:92:
Frama_C_show_each_lt: Frama_C_show_each_lt:
[-0x1.4000000000000p3 .. -0x0.0000000000000p-1022], [-0x1.4000000000000p3 .. -0x0.0000000000000p0],
[-0x1.fffffffffffffp1023 .. 0x0.0000000000000p-1022] [-0x1.fffffffffffffp1023 .. 0x0.0000000000000p0]
[eva] tests/float/logic.i:96: [eva] tests/float/logic.i:96:
Frama_C_show_each_eq_double: Frama_C_show_each_eq_double:
[-0x1.4000000000000p3 .. -0x0.0000000000000p-1022], [-0x1.4000000000000p3 .. -0x0.0000000000000p0],
[-0x1.4000000000000p3 .. 0x0.0000000000000p-1022] [-0x1.4000000000000p3 .. 0x0.0000000000000p0]
[eva] tests/float/logic.i:100: [eva] tests/float/logic.i:100:
Frama_C_show_each_lt_double: Frama_C_show_each_lt_double:
[-0x1.4000000000000p3 .. -0x0.0000000000000p-1022], [-0x1.4000000000000p3 .. -0x0.0000000000000p0],
[-0x1.fffffffffffffp1023 .. -0x0.0000000000001p-1022] [-0x1.fffffffffffffp1023 .. -0x0.0000000000001p-1022]
[eva] tests/float/logic.i:104: [eva] tests/float/logic.i:104:
Frama_C_show_each_le_double: Frama_C_show_each_le_double:
[-0x1.4000000000000p3 .. -0x0.0000000000000p-1022], [-0x1.4000000000000p3 .. -0x0.0000000000000p0],
[-0x1.fffffffffffffp1023 .. 0x0.0000000000000p-1022] [-0x1.fffffffffffffp1023 .. 0x0.0000000000000p0]
[eva] tests/float/logic.i:108: [eva] tests/float/logic.i:108:
Frama_C_show_each_ne_double: Frama_C_show_each_ne_double:
[-0x1.4000000000000p3 .. -0x0.0000000000000p-1022], [-0x1.4000000000000p3 .. -0x0.0000000000000p0],
[-0x1.fffffffffffffp1023 .. 0x1.fffffffffffffp1023] [-0x1.fffffffffffffp1023 .. 0x1.fffffffffffffp1023]
[eva] Recording results for test_comparison_reduction [eva] Recording results for test_comparison_reduction
[eva] Done for function test_comparison_reduction [eva] Done for function test_comparison_reduction
...@@ -261,31 +252,31 @@ ...@@ -261,31 +252,31 @@
Called from tests/float/logic.i:128. Called from tests/float/logic.i:128.
[eva] tests/float/logic.i:84: [eva] tests/float/logic.i:84:
Frama_C_show_each_eq: Frama_C_show_each_eq:
[-0x1.4000000000000p3 .. 0x0.0000000000000p-1022], [-0x1.4000000000000p3 .. 0x0.0000000000000p0],
[-0x1.4000000000000p3 .. 0x0.0000000000000p-1022] [-0x1.4000000000000p3 .. 0x0.0000000000000p0]
[eva] tests/float/logic.i:88: [eva] tests/float/logic.i:88:
Frama_C_show_each_lt: Frama_C_show_each_lt:
[-0x1.4000000000000p3 .. 0x0.0000000000000p-1022], [-0x1.4000000000000p3 .. 0x0.0000000000000p0],
[-0x1.fffffffffffffp1023 .. -0x0.0000000000001p-1022] [-0x1.fffffffffffffp1023 .. -0x0.0000000000001p-1022]
[eva] tests/float/logic.i:92: [eva] tests/float/logic.i:92:
Frama_C_show_each_lt: Frama_C_show_each_lt:
[-0x1.4000000000000p3 .. 0x0.0000000000000p-1022], [-0x1.4000000000000p3 .. 0x0.0000000000000p0],
[-0x1.fffffffffffffp1023 .. 0x0.0000000000000p-1022] [-0x1.fffffffffffffp1023 .. 0x0.0000000000000p0]
[eva] tests/float/logic.i:96: [eva] tests/float/logic.i:96:
Frama_C_show_each_eq_double: Frama_C_show_each_eq_double:
[-0x1.4000000000000p3 .. 0x0.0000000000000p-1022], [-0x1.4000000000000p3 .. 0x0.0000000000000p0],
[-0x1.4000000000000p3 .. 0x0.0000000000000p-1022] [-0x1.4000000000000p3 .. 0x0.0000000000000p0]
[eva] tests/float/logic.i:100: [eva] tests/float/logic.i:100:
Frama_C_show_each_lt_double: Frama_C_show_each_lt_double:
[-0x1.4000000000000p3 .. 0x0.0000000000000p-1022], [-0x1.4000000000000p3 .. 0x0.0000000000000p0],
[-0x1.fffffffffffffp1023 .. -0x0.0000000000001p-1022] [-0x1.fffffffffffffp1023 .. -0x0.0000000000001p-1022]
[eva] tests/float/logic.i:104: [eva] tests/float/logic.i:104:
Frama_C_show_each_le_double: Frama_C_show_each_le_double:
[-0x1.4000000000000p3 .. 0x0.0000000000000p-1022], [-0x1.4000000000000p3 .. 0x0.0000000000000p0],
[-0x1.fffffffffffffp1023 .. 0x0.0000000000000p-1022] [-0x1.fffffffffffffp1023 .. 0x0.0000000000000p0]
[eva] tests/float/logic.i:108: [eva] tests/float/logic.i:108:
Frama_C_show_each_ne_double: Frama_C_show_each_ne_double:
[-0x1.4000000000000p3 .. 0x0.0000000000000p-1022], [-0x1.4000000000000p3 .. 0x0.0000000000000p0],
[-0x1.fffffffffffffp1023 .. 0x1.fffffffffffffp1023] [-0x1.fffffffffffffp1023 .. 0x1.fffffffffffffp1023]
[eva] Recording results for test_comparison_reduction [eva] Recording results for test_comparison_reduction
[eva] Done for function test_comparison_reduction [eva] Done for function test_comparison_reduction
...@@ -368,7 +359,7 @@ ...@@ -368,7 +359,7 @@
__retres ∈ {-0x1.bca1b00000000p-1} __retres ∈ {-0x1.bca1b00000000p-1}
[eva:final-states] Values at end of function test_comparison_evaluation: [eva:final-states] Values at end of function test_comparison_evaluation:
zero ∈ {0} zero ∈ {0}
minus_zero ∈ {-0x0.0000000000000p-1022} minus_zero ∈ {-0x0.0000000000000p0}
one ∈ {0x1.0000000000000p0} one ∈ {0x1.0000000000000p0}
higher ∈ [0x1.91eb860000000p1 .. 0x1.9000000000000p3] higher ∈ [0x1.91eb860000000p1 .. 0x1.9000000000000p3]
middle ∈ [-0x1.91eb860000000p1 .. 0x1.91eb860000000p1] middle ∈ [-0x1.91eb860000000p1 .. 0x1.91eb860000000p1]
......
tests/float/oracle/logic.1.res.oracle
+ 26
− 30
View file @ 9366f3cf
...@@ -116,24 +116,22 @@ ...@@ -116,24 +116,22 @@
test_builtin_comparisons <- main. test_builtin_comparisons <- main.
Called from tests/float/logic.i:118. Called from tests/float/logic.i:118.
[eva] tests/float/logic.i:84: [eva] tests/float/logic.i:84:
Frama_C_show_each_eq: {-0x0.0000000000000p-1022}, [-inf .. inf] ∪ {NaN} Frama_C_show_each_eq: {-0x0.0000000000000p0}, [-inf .. inf] ∪ {NaN}
[eva] tests/float/logic.i:88: [eva] tests/float/logic.i:88:
Frama_C_show_each_lt: {-0x0.0000000000000p-1022}, [-inf .. inf] ∪ {NaN} Frama_C_show_each_lt: {-0x0.0000000000000p0}, [-inf .. inf] ∪ {NaN}
[eva] tests/float/logic.i:92: [eva] tests/float/logic.i:92:
Frama_C_show_each_lt: {-0x0.0000000000000p-1022}, [-inf .. inf] ∪ {NaN} Frama_C_show_each_lt: {-0x0.0000000000000p0}, [-inf .. inf] ∪ {NaN}
[eva] tests/float/logic.i:96: [eva] tests/float/logic.i:96:
Frama_C_show_each_eq_double: Frama_C_show_each_eq_double:
{-0x0.0000000000000p-1022}, {-0x0.0000000000000p0}, [-0x0.0000000000000p0 .. 0x0.0000000000000p0]
[-0x0.0000000000000p-1022 .. 0x0.0000000000000p-1022]
[eva] tests/float/logic.i:100: [eva] tests/float/logic.i:100:
Frama_C_show_each_lt_double: Frama_C_show_each_lt_double:
{-0x0.0000000000000p-1022}, [-inf .. -0x0.0000000000001p-1022] {-0x0.0000000000000p0}, [-inf .. -0x0.0000000000001p-1022]
[eva] tests/float/logic.i:104: [eva] tests/float/logic.i:104:
Frama_C_show_each_le_double: Frama_C_show_each_le_double:
{-0x0.0000000000000p-1022}, [-inf .. 0x0.0000000000000p-1022] {-0x0.0000000000000p0}, [-inf .. 0x0.0000000000000p0]
[eva] tests/float/logic.i:108: [eva] tests/float/logic.i:108:
Frama_C_show_each_ne_double: Frama_C_show_each_ne_double: {-0x0.0000000000000p0}, [-inf .. inf] ∪ {NaN}
{-0x0.0000000000000p-1022}, [-inf .. inf] ∪ {NaN}
[eva] Recording results for test_comparison_reduction [eva] Recording results for test_comparison_reduction
[eva] Done for function test_comparison_reduction [eva] Done for function test_comparison_reduction
[eva] computing for function test_comparison_reduction <- [eva] computing for function test_comparison_reduction <-
...@@ -144,11 +142,11 @@ ...@@ -144,11 +142,11 @@
[eva] tests/float/logic.i:92: Frama_C_show_each_lt: {0}, [-inf .. inf] ∪ {NaN} [eva] tests/float/logic.i:92: Frama_C_show_each_lt: {0}, [-inf .. inf] ∪ {NaN}
[eva] tests/float/logic.i:96: [eva] tests/float/logic.i:96:
Frama_C_show_each_eq_double: Frama_C_show_each_eq_double:
{0}, [-0x0.0000000000000p-1022 .. 0x0.0000000000000p-1022] {0}, [-0x0.0000000000000p0 .. 0x0.0000000000000p0]
[eva] tests/float/logic.i:100: [eva] tests/float/logic.i:100:
Frama_C_show_each_lt_double: {0}, [-inf .. -0x0.0000000000001p-1022] Frama_C_show_each_lt_double: {0}, [-inf .. -0x0.0000000000001p-1022]
[eva] tests/float/logic.i:104: [eva] tests/float/logic.i:104:
Frama_C_show_each_le_double: {0}, [-inf .. 0x0.0000000000000p-1022] Frama_C_show_each_le_double: {0}, [-inf .. 0x0.0000000000000p0]
[eva] tests/float/logic.i:108: [eva] tests/float/logic.i:108:
Frama_C_show_each_ne_double: {0}, [-inf .. inf] ∪ {NaN} Frama_C_show_each_ne_double: {0}, [-inf .. inf] ∪ {NaN}
[eva] Recording results for test_comparison_reduction [eva] Recording results for test_comparison_reduction
...@@ -208,28 +206,27 @@ ...@@ -208,28 +206,27 @@
Called from tests/float/logic.i:126. Called from tests/float/logic.i:126.
[eva] tests/float/logic.i:84: [eva] tests/float/logic.i:84:
Frama_C_show_each_eq: Frama_C_show_each_eq:
[-0x1.4000000000000p3 .. -0x0.0000000000000p-1022], [-inf .. inf] ∪ {NaN} [-0x1.4000000000000p3 .. -0x0.0000000000000p0], [-inf .. inf] ∪ {NaN}
[eva] tests/float/logic.i:88: [eva] tests/float/logic.i:88:
Frama_C_show_each_lt: Frama_C_show_each_lt:
[-0x1.4000000000000p3 .. -0x0.0000000000000p-1022], [-inf .. inf] ∪ {NaN} [-0x1.4000000000000p3 .. -0x0.0000000000000p0], [-inf .. inf] ∪ {NaN}
[eva] tests/float/logic.i:92: [eva] tests/float/logic.i:92:
Frama_C_show_each_lt: Frama_C_show_each_lt:
[-0x1.4000000000000p3 .. -0x0.0000000000000p-1022], [-inf .. inf] ∪ {NaN} [-0x1.4000000000000p3 .. -0x0.0000000000000p0], [-inf .. inf] ∪ {NaN}
[eva] tests/float/logic.i:96: [eva] tests/float/logic.i:96:
Frama_C_show_each_eq_double: Frama_C_show_each_eq_double:
[-0x1.4000000000000p3 .. -0x0.0000000000000p-1022], [-0x1.4000000000000p3 .. -0x0.0000000000000p0],
[-0x1.4000000000000p3 .. 0x0.0000000000000p-1022] [-0x1.4000000000000p3 .. 0x0.0000000000000p0]
[eva] tests/float/logic.i:100: [eva] tests/float/logic.i:100:
Frama_C_show_each_lt_double: Frama_C_show_each_lt_double:
[-0x1.4000000000000p3 .. -0x0.0000000000000p-1022], [-0x1.4000000000000p3 .. -0x0.0000000000000p0],
[-inf .. -0x0.0000000000001p-1022] [-inf .. -0x0.0000000000001p-1022]
[eva] tests/float/logic.i:104: [eva] tests/float/logic.i:104:
Frama_C_show_each_le_double: Frama_C_show_each_le_double:
[-0x1.4000000000000p3 .. -0x0.0000000000000p-1022], [-0x1.4000000000000p3 .. -0x0.0000000000000p0], [-inf .. 0x0.0000000000000p0]
[-inf .. 0x0.0000000000000p-1022]
[eva] tests/float/logic.i:108: [eva] tests/float/logic.i:108:
Frama_C_show_each_ne_double: Frama_C_show_each_ne_double:
[-0x1.4000000000000p3 .. -0x0.0000000000000p-1022], [-inf .. inf] ∪ {NaN} [-0x1.4000000000000p3 .. -0x0.0000000000000p0], [-inf .. inf] ∪ {NaN}
[eva] Recording results for test_comparison_reduction [eva] Recording results for test_comparison_reduction
[eva] Done for function test_comparison_reduction [eva] Done for function test_comparison_reduction
[eva] computing for function test_comparison_reduction <- [eva] computing for function test_comparison_reduction <-
...@@ -237,28 +234,27 @@ ...@@ -237,28 +234,27 @@
Called from tests/float/logic.i:128. Called from tests/float/logic.i:128.
[eva] tests/float/logic.i:84: [eva] tests/float/logic.i:84:
Frama_C_show_each_eq: Frama_C_show_each_eq:
[-0x1.4000000000000p3 .. 0x0.0000000000000p-1022], [-inf .. inf] ∪ {NaN} [-0x1.4000000000000p3 .. 0x0.0000000000000p0], [-inf .. inf] ∪ {NaN}
[eva] tests/float/logic.i:88: [eva] tests/float/logic.i:88:
Frama_C_show_each_lt: Frama_C_show_each_lt:
[-0x1.4000000000000p3 .. 0x0.0000000000000p-1022], [-inf .. inf] ∪ {NaN} [-0x1.4000000000000p3 .. 0x0.0000000000000p0], [-inf .. inf] ∪ {NaN}
[eva] tests/float/logic.i:92: [eva] tests/float/logic.i:92:
Frama_C_show_each_lt: Frama_C_show_each_lt:
[-0x1.4000000000000p3 .. 0x0.0000000000000p-1022], [-inf .. inf] ∪ {NaN} [-0x1.4000000000000p3 .. 0x0.0000000000000p0], [-inf .. inf] ∪ {NaN}
[eva] tests/float/logic.i:96: [eva] tests/float/logic.i:96:
Frama_C_show_each_eq_double: Frama_C_show_each_eq_double:
[-0x1.4000000000000p3 .. 0x0.0000000000000p-1022], [-0x1.4000000000000p3 .. 0x0.0000000000000p0],
[-0x1.4000000000000p3 .. 0x0.0000000000000p-1022] [-0x1.4000000000000p3 .. 0x0.0000000000000p0]
[eva] tests/float/logic.i:100: [eva] tests/float/logic.i:100:
Frama_C_show_each_lt_double: Frama_C_show_each_lt_double:
[-0x1.4000000000000p3 .. 0x0.0000000000000p-1022], [-0x1.4000000000000p3 .. 0x0.0000000000000p0],
[-inf .. -0x0.0000000000001p-1022] [-inf .. -0x0.0000000000001p-1022]
[eva] tests/float/logic.i:104: [eva] tests/float/logic.i:104:
Frama_C_show_each_le_double: Frama_C_show_each_le_double:
[-0x1.4000000000000p3 .. 0x0.0000000000000p-1022], [-0x1.4000000000000p3 .. 0x0.0000000000000p0], [-inf .. 0x0.0000000000000p0]
[-inf .. 0x0.0000000000000p-1022]
[eva] tests/float/logic.i:108: [eva] tests/float/logic.i:108:
Frama_C_show_each_ne_double: Frama_C_show_each_ne_double:
[-0x1.4000000000000p3 .. 0x0.0000000000000p-1022], [-inf .. inf] ∪ {NaN} [-0x1.4000000000000p3 .. 0x0.0000000000000p0], [-inf .. inf] ∪ {NaN}
[eva] Recording results for test_comparison_reduction [eva] Recording results for test_comparison_reduction
[eva] Done for function test_comparison_reduction [eva] Done for function test_comparison_reduction
[eva] computing for function test_comparison_reduction <- [eva] computing for function test_comparison_reduction <-
...@@ -368,7 +364,7 @@ ...@@ -368,7 +364,7 @@
__retres ∈ {-0x1.bca1b00000000p-1} __retres ∈ {-0x1.bca1b00000000p-1}
[eva:final-states] Values at end of function test_comparison_evaluation: [eva:final-states] Values at end of function test_comparison_evaluation:
zero ∈ {0} zero ∈ {0}
minus_zero ∈ {-0x0.0000000000000p-1022} minus_zero ∈ {-0x0.0000000000000p0}
one ∈ {0x1.0000000000000p0} one ∈ {0x1.0000000000000p0}
higher ∈ [0x1.91eb860000000p1 .. 0x1.9000000000000p3] higher ∈ [0x1.91eb860000000p1 .. 0x1.9000000000000p3]
middle ∈ [-0x1.91eb860000000p1 .. 0x1.91eb860000000p1] middle ∈ [-0x1.91eb860000000p1 .. 0x1.91eb860000000p1]
......
tests/float/oracle/nonlin.0.res.oracle
+ 3
− 3
View file @ 9366f3cf
...@@ -247,7 +247,7 @@ ...@@ -247,7 +247,7 @@
[eva:final-states] Values at end of function around_zeros: [eva:final-states] Values at end of function around_zeros:
Frama_C_entropy_source ∈ [--..--] Frama_C_entropy_source ∈ [--..--]
f1 ∈ {0x1.0000000000000p-149} f1 ∈ {0x1.0000000000000p-149}
f ∈ [-0x0.0000000000000p-1022 .. 0x1.0000000000000p-149] f ∈ [-0x0.0000000000000p0 .. 0x1.0000000000000p-149]
res ∈ [-0x1.fffffe0000000p127 .. 0x1.fffffe0000000p127] res ∈ [-0x1.fffffe0000000p127 .. 0x1.fffffe0000000p127]
[eva:final-states] Values at end of function garbled: [eva:final-states] Values at end of function garbled:
a_0 ∈ a_0 ∈
...@@ -257,7 +257,7 @@ ...@@ -257,7 +257,7 @@
[eva:final-states] Values at end of function nonlin_f: [eva:final-states] Values at end of function nonlin_f:
Frama_C_entropy_source ∈ [--..--] Frama_C_entropy_source ∈ [--..--]
a ∈ [0x1.4000000000000p2 .. 0x1.c000000000000p2] a ∈ [0x1.4000000000000p2 .. 0x1.c000000000000p2]
b ∈ [-0x0.0000000000000p-1022 .. 0x1.0000000000000p0] b ∈ [-0x0.0000000000000p0 .. 0x1.0000000000000p0]
c ∈ {0x1.c000000000000p2} c ∈ {0x1.c000000000000p2}
r1 ∈ [0x1.4000000000000p2 .. 0x1.2000000000000p3] r1 ∈ [0x1.4000000000000p2 .. 0x1.2000000000000p3]
r2 ∈ [0x1.4000000000000p2 .. 0x1.c800000000000p2] r2 ∈ [0x1.4000000000000p2 .. 0x1.c800000000000p2]
...@@ -286,7 +286,7 @@ ...@@ -286,7 +286,7 @@
[eva:final-states] Values at end of function main: [eva:final-states] Values at end of function main:
Frama_C_entropy_source ∈ [--..--] Frama_C_entropy_source ∈ [--..--]
a ∈ [0x1.4000000000000p2 .. 0x1.c000000000000p2] a ∈ [0x1.4000000000000p2 .. 0x1.c000000000000p2]
b ∈ [-0x0.0000000000000p-1022 .. 0x1.0000000000000p0] b ∈ [-0x0.0000000000000p0 .. 0x1.0000000000000p0]
c ∈ {0x1.c000000000000p2} c ∈ {0x1.c000000000000p2}
r1 ∈ [0x1.4000000000000p2 .. 0x1.2000000000000p3] r1 ∈ [0x1.4000000000000p2 .. 0x1.2000000000000p3]
r2 ∈ [0x1.4000000000000p2 .. 0x1.c800000000000p2] r2 ∈ [0x1.4000000000000p2 .. 0x1.c800000000000p2]
......
tests/float/oracle/nonlin.1.res.oracle
+ 4
− 4
View file @ 9366f3cf
...@@ -270,7 +270,7 @@ ...@@ -270,7 +270,7 @@
[eva:final-states] Values at end of function around_zeros: [eva:final-states] Values at end of function around_zeros:
Frama_C_entropy_source ∈ [--..--] Frama_C_entropy_source ∈ [--..--]
f1 ∈ {0x1.0000000000000p-149} f1 ∈ {0x1.0000000000000p-149}
f ∈ [-0x0.0000000000000p-1022 .. 0x0.0000000000000p-1022] f ∈ [-0x0.0000000000000p0 .. 0x0.0000000000000p0]
res ∈ {-0x1.0000000000000p0} res ∈ {-0x1.0000000000000p0}
[eva:final-states] Values at end of function garbled: [eva:final-states] Values at end of function garbled:
a_0 ∈ a_0 ∈
...@@ -280,7 +280,7 @@ ...@@ -280,7 +280,7 @@
[eva:final-states] Values at end of function nonlin_f: [eva:final-states] Values at end of function nonlin_f:
Frama_C_entropy_source ∈ [--..--] Frama_C_entropy_source ∈ [--..--]
a ∈ [0x1.4000000000000p2 .. 0x1.c000000000000p2] a ∈ [0x1.4000000000000p2 .. 0x1.c000000000000p2]
b ∈ [-0x0.0000000000000p-1022 .. 0x1.0000000000000p0] b ∈ [-0x0.0000000000000p0 .. 0x1.0000000000000p0]
c ∈ {0x1.c000000000000p2} c ∈ {0x1.c000000000000p2}
r1 ∈ [0x1.4000000000000p2 .. 0x1.cffffffffffffp2] r1 ∈ [0x1.4000000000000p2 .. 0x1.cffffffffffffp2]
r2 ∈ [0x1.4000000000000p2 .. 0x1.c0fffffffffffp2] r2 ∈ [0x1.4000000000000p2 .. 0x1.c0fffffffffffp2]
...@@ -288,7 +288,7 @@ ...@@ -288,7 +288,7 @@
[eva:final-states] Values at end of function norm: [eva:final-states] Values at end of function norm:
v1 ∈ [-0x1.fffffe0000000p127 .. 0x1.fffffe0000000p127] v1 ∈ [-0x1.fffffe0000000p127 .. 0x1.fffffe0000000p127]
v2 ∈ [-0x1.fffffe0000000p127 .. 0x1.fffffe0000000p127] v2 ∈ [-0x1.fffffe0000000p127 .. 0x1.fffffe0000000p127]
square ∈ [-0x0.0000000000000p-1022 .. 0x1.fffffc0000020p256] square ∈ [-0x0.0000000000000p0 .. 0x1.fffffc0000020p256]
[eva:final-states] Values at end of function other: [eva:final-states] Values at end of function other:
Frama_C_entropy_source ∈ [--..--] Frama_C_entropy_source ∈ [--..--]
i ∈ [-0x1.714fffffffff7p1 .. 0x1.71c0000000003p1] i ∈ [-0x1.714fffffffff7p1 .. 0x1.71c0000000003p1]
...@@ -309,7 +309,7 @@ ...@@ -309,7 +309,7 @@
[eva:final-states] Values at end of function main: [eva:final-states] Values at end of function main:
Frama_C_entropy_source ∈ [--..--] Frama_C_entropy_source ∈ [--..--]
a ∈ [0x1.4000000000000p2 .. 0x1.c000000000000p2] a ∈ [0x1.4000000000000p2 .. 0x1.c000000000000p2]
b ∈ [-0x0.0000000000000p-1022 .. 0x1.0000000000000p0] b ∈ [-0x0.0000000000000p0 .. 0x1.0000000000000p0]
c ∈ {0x1.c000000000000p2} c ∈ {0x1.c000000000000p2}
r1 ∈ [0x1.4000000000000p2 .. 0x1.cffffffffffffp2] r1 ∈ [0x1.4000000000000p2 .. 0x1.cffffffffffffp2]
r2 ∈ [0x1.4000000000000p2 .. 0x1.c0fffffffffffp2] r2 ∈ [0x1.4000000000000p2 .. 0x1.c0fffffffffffp2]
......
tests/float/oracle/nonlin.2.res.oracle
+ 3
− 3
View file @ 9366f3cf
...@@ -247,7 +247,7 @@ ...@@ -247,7 +247,7 @@
[eva:final-states] Values at end of function around_zeros: [eva:final-states] Values at end of function around_zeros:
Frama_C_entropy_source ∈ [--..--] Frama_C_entropy_source ∈ [--..--]
f1 ∈ {0x1.0000000000000p-149} f1 ∈ {0x1.0000000000000p-149}
f ∈ [-0x0.0000000000000p-1022 .. 0x1.0000000000000p-149] f ∈ [-0x0.0000000000000p0 .. 0x1.0000000000000p-149]
res ∈ [-0x1.fffffe0000000p127 .. 0x1.fffffe0000000p127] res ∈ [-0x1.fffffe0000000p127 .. 0x1.fffffe0000000p127]
[eva:final-states] Values at end of function garbled: [eva:final-states] Values at end of function garbled:
a_0 ∈ a_0 ∈
...@@ -257,7 +257,7 @@ ...@@ -257,7 +257,7 @@
[eva:final-states] Values at end of function nonlin_f: [eva:final-states] Values at end of function nonlin_f:
Frama_C_entropy_source ∈ [--..--] Frama_C_entropy_source ∈ [--..--]
a ∈ [0x1.4000000000000p2 .. 0x1.c000000000000p2] a ∈ [0x1.4000000000000p2 .. 0x1.c000000000000p2]
b ∈ [-0x0.0000000000000p-1022 .. 0x1.0000000000000p0] b ∈ [-0x0.0000000000000p0 .. 0x1.0000000000000p0]
c ∈ {0x1.c000000000000p2} c ∈ {0x1.c000000000000p2}
r1 ∈ [0x1.4000000000000p2 .. 0x1.2000000000000p3] r1 ∈ [0x1.4000000000000p2 .. 0x1.2000000000000p3]
r2 ∈ [0x1.4000000000000p2 .. 0x1.c800000000000p2] r2 ∈ [0x1.4000000000000p2 .. 0x1.c800000000000p2]
...@@ -286,7 +286,7 @@ ...@@ -286,7 +286,7 @@
[eva:final-states] Values at end of function main: [eva:final-states] Values at end of function main:
Frama_C_entropy_source ∈ [--..--] Frama_C_entropy_source ∈ [--..--]
a ∈ [0x1.4000000000000p2 .. 0x1.c000000000000p2] a ∈ [0x1.4000000000000p2 .. 0x1.c000000000000p2]
b ∈ [-0x0.0000000000000p-1022 .. 0x1.0000000000000p0] b ∈ [-0x0.0000000000000p0 .. 0x1.0000000000000p0]
c ∈ {0x1.c000000000000p2} c ∈ {0x1.c000000000000p2}
r1 ∈ [0x1.4000000000000p2 .. 0x1.2000000000000p3] r1 ∈ [0x1.4000000000000p2 .. 0x1.2000000000000p3]
r2 ∈ [0x1.4000000000000p2 .. 0x1.c800000000000p2] r2 ∈ [0x1.4000000000000p2 .. 0x1.c800000000000p2]
......
tests/float/oracle/nonlin.3.res.oracle
+ 4
− 4
View file @ 9366f3cf
...@@ -270,7 +270,7 @@ ...@@ -270,7 +270,7 @@
[eva:final-states] Values at end of function around_zeros: [eva:final-states] Values at end of function around_zeros:
Frama_C_entropy_source ∈ [--..--] Frama_C_entropy_source ∈ [--..--]
f1 ∈ {0x1.0000000000000p-149} f1 ∈ {0x1.0000000000000p-149}
f ∈ [-0x0.0000000000000p-1022 .. 0x0.0000000000000p-1022] f ∈ [-0x0.0000000000000p0 .. 0x0.0000000000000p0]
res ∈ {-0x1.0000000000000p0} res ∈ {-0x1.0000000000000p0}
[eva:final-states] Values at end of function garbled: [eva:final-states] Values at end of function garbled:
a_0 ∈ a_0 ∈
...@@ -280,7 +280,7 @@ ...@@ -280,7 +280,7 @@
[eva:final-states] Values at end of function nonlin_f: [eva:final-states] Values at end of function nonlin_f:
Frama_C_entropy_source ∈ [--..--] Frama_C_entropy_source ∈ [--..--]
a ∈ [0x1.4000000000000p2 .. 0x1.c000000000000p2] a ∈ [0x1.4000000000000p2 .. 0x1.c000000000000p2]
b ∈ [-0x0.0000000000000p-1022 .. 0x1.0000000000000p0] b ∈ [-0x0.0000000000000p0 .. 0x1.0000000000000p0]
c ∈ {0x1.c000000000000p2} c ∈ {0x1.c000000000000p2}
r1 ∈ [0x1.4000000000000p2 .. 0x1.cffffe0000000p2] r1 ∈ [0x1.4000000000000p2 .. 0x1.cffffe0000000p2]
r2 ∈ [0x1.4000000000000p2 .. 0x1.c0fffe0000000p2] r2 ∈ [0x1.4000000000000p2 .. 0x1.c0fffe0000000p2]
...@@ -288,7 +288,7 @@ ...@@ -288,7 +288,7 @@
[eva:final-states] Values at end of function norm: [eva:final-states] Values at end of function norm:
v1 ∈ [-0x1.fffffe0000000p127 .. 0x1.fffffe0000000p127] v1 ∈ [-0x1.fffffe0000000p127 .. 0x1.fffffe0000000p127]
v2 ∈ [-0x1.fffffe0000000p127 .. 0x1.fffffe0000000p127] v2 ∈ [-0x1.fffffe0000000p127 .. 0x1.fffffe0000000p127]
square ∈ [-0x0.0000000000000p-1022 .. 0x1.fffffc0000020p256] square ∈ [-0x0.0000000000000p0 .. 0x1.fffffc0000020p256]
[eva:final-states] Values at end of function other: [eva:final-states] Values at end of function other:
Frama_C_entropy_source ∈ [--..--] Frama_C_entropy_source ∈ [--..--]
i ∈ [-0x1.714fee0000000p1 .. 0x1.71c0040000000p1] i ∈ [-0x1.714fee0000000p1 .. 0x1.71c0040000000p1]
...@@ -309,7 +309,7 @@ ...@@ -309,7 +309,7 @@
[eva:final-states] Values at end of function main: [eva:final-states] Values at end of function main:
Frama_C_entropy_source ∈ [--..--] Frama_C_entropy_source ∈ [--..--]
a ∈ [0x1.4000000000000p2 .. 0x1.c000000000000p2] a ∈ [0x1.4000000000000p2 .. 0x1.c000000000000p2]
b ∈ [-0x0.0000000000000p-1022 .. 0x1.0000000000000p0] b ∈ [-0x0.0000000000000p0 .. 0x1.0000000000000p0]
c ∈ {0x1.c000000000000p2} c ∈ {0x1.c000000000000p2}
r1 ∈ [0x1.4000000000000p2 .. 0x1.cffffe0000000p2] r1 ∈ [0x1.4000000000000p2 .. 0x1.cffffe0000000p2]
r2 ∈ [0x1.4000000000000p2 .. 0x1.c0fffe0000000p2] r2 ∈ [0x1.4000000000000p2 .. 0x1.c0fffe0000000p2]
......
tests/value/oracle/cond_integer_cast_of_float.res.oracle
+ 3
− 3
View file @ 9366f3cf
...@@ -152,7 +152,7 @@ ...@@ -152,7 +152,7 @@
[eva] tests/value/cond_integer_cast_of_float.i:17: [eva] tests/value/cond_integer_cast_of_float.i:17:
Frama_C_show_each_float_: [0x1.0000000000000p1 .. 0x1.0000000000000p3] Frama_C_show_each_float_: [0x1.0000000000000p1 .. 0x1.0000000000000p3]
[eva] tests/value/cond_integer_cast_of_float.i:20: [eva] tests/value/cond_integer_cast_of_float.i:20:
Frama_C_show_each_float_: [-0x0.0000000000000p-1022 .. 0x1.3ffffe0000000p2] Frama_C_show_each_float_: [-0x0.0000000000000p0 .. 0x1.3ffffe0000000p2]
[eva] tests/value/cond_integer_cast_of_float.i:23: [eva] tests/value/cond_integer_cast_of_float.i:23:
Frama_C_show_each_float_: [0x1.0000000000000p0 .. 0x1.0000000000000p3] Frama_C_show_each_float_: [0x1.0000000000000p0 .. 0x1.0000000000000p3]
[eva] tests/value/cond_integer_cast_of_float.i:26: [eva] tests/value/cond_integer_cast_of_float.i:26:
...@@ -160,13 +160,13 @@ ...@@ -160,13 +160,13 @@
[eva] tests/value/cond_integer_cast_of_float.i:29: [eva] tests/value/cond_integer_cast_of_float.i:29:
Frama_C_show_each_double: [0x1.0000000000000p1 .. 0x1.0000000000000p3] Frama_C_show_each_double: [0x1.0000000000000p1 .. 0x1.0000000000000p3]
[eva] tests/value/cond_integer_cast_of_float.i:32: [eva] tests/value/cond_integer_cast_of_float.i:32:
Frama_C_show_each_double: [-0x0.0000000000000p-1022 .. 0x1.3ffffffffffffp2] Frama_C_show_each_double: [-0x0.0000000000000p0 .. 0x1.3ffffffffffffp2]
[eva] tests/value/cond_integer_cast_of_float.i:35: [eva] tests/value/cond_integer_cast_of_float.i:35:
Frama_C_show_each_double: [0x1.0000000000000p0 .. 0x1.0000000000000p3] Frama_C_show_each_double: [0x1.0000000000000p0 .. 0x1.0000000000000p3]
[eva] tests/value/cond_integer_cast_of_float.i:38: [eva] tests/value/cond_integer_cast_of_float.i:38:
Frama_C_show_each_double: [0x1.8000000000000p1 .. 0x1.fffffffffffffp1] Frama_C_show_each_double: [0x1.8000000000000p1 .. 0x1.fffffffffffffp1]
[eva] tests/value/cond_integer_cast_of_float.i:73: [eva] tests/value/cond_integer_cast_of_float.i:73:
Frama_C_show_each: [-0x0.0000000000000p-1022 .. 0x1.0000000000000p3], [0..8] Frama_C_show_each: [-0x0.0000000000000p0 .. 0x1.0000000000000p3], [0..8]
[eva] Recording results for main1 [eva] Recording results for main1
[eva] Done for function main1 [eva] Done for function main1
[eva] computing for function main2 <- main <- mainbis. [eva] computing for function main2 <- main <- mainbis.
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment