diff --git a/src/libraries/utils/floating_point.ml b/src/libraries/utils/floating_point.ml
index 9d5399133a88d812663316acd729259e4f6585f3..3a87fedd855315e79ef10b129648cc28303bd653 100644
--- a/src/libraries/utils/floating_point.ml
+++ b/src/libraries/utils/floating_point.ml
@@ -295,7 +295,7 @@ let pretty_normal ~use_hex fmt f =
let firstdigit, exp =
if exp <> 0
then 1, (exp - 1023)
- else 0, -1022
+ else 0, if f = 0. then 0 else -1022
in
if not use_hex
then begin
diff --git a/tests/float/oracle/cond.res.oracle b/tests/float/oracle/cond.res.oracle
index 707cac7a8bd634103f9af0eb5ba13fc7b832ec50..fb36e697b14e57cb73e252497ad700c8b8a48120 100644
--- a/tests/float/oracle/cond.res.oracle
+++ b/tests/float/oracle/cond.res.oracle
@@ -40,7 +40,7 @@
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
Frama_C_entropy_source ∈ [--..--]
- x ∈ [-0x0.0000000000000p-1022 .. 0x1.4000000000000p3]
+ x ∈ [-0x0.0000000000000p0 .. 0x1.4000000000000p3]
dx ∈ [0x1.0000000000001p0 .. 0x1.4000000000000p3]
dz ∈ [0x1.0000000000001p0 .. 0x1.4000000000000p3]
dt ∈ [-0x1.4000000000000p3 .. 0x1.fffffffffffffp-1]
diff --git a/tests/float/oracle/const.res.oracle b/tests/float/oracle/const.res.oracle
index e70a11cc85789fe4df7c48f86c096f1b1f5eb73c..82eb8a1af5e2752e2a6ab2025df18f5de5ee051c 100644
--- a/tests/float/oracle/const.res.oracle
+++ b/tests/float/oracle/const.res.oracle
@@ -1,10 +1,10 @@
[kernel] Parsing tests/float/const.i (no preprocessing)
[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:
Floating-point constant 0.000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000002470328229206232720882843964341106861825299013071623822127928412503377536351043759326499181808179961898982823477228588654633283551779698981993873980053909390631503565951557022639229085839244910518443593180284993653615250031937045767824921936562366986365848075700158576926990370631192827955855133292783433840935197801553124659726357957462276646527282722005637400648549997709659947045402082816622623785739345073633900796776193057750674017632467360096895134053553745851666113422376667860416215968046191446729184030053005753084904876539171138659164623952491262365388187963623937328042389101867234849766823508986338858792562830275599565752445550725518931369083625477918694866799496832404970582102851318545139621383772282614543769341253209859132766723632812501 is not represented exactly. Will use 0x0.0000000000001p-1022.
[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:
Floating-point constant 0.0000000000000000000000000000000000000000000014012984643248170709237295832899161312802619418765157717570682838897910826858606014866381883621215820312499 is not represented exactly. Will use 0x1.0000000000000p-149.
[kernel:parser:decimal-float] tests/float/const.i:27: Warning:
@@ -18,9 +18,9 @@
[kernel:parser:decimal-float] tests/float/const.i:34: Warning:
Floating-point constant 0.00000000000000000000000000000000000000000000070064923216240853546186479164495806564013097093825788587853414194489554134293030074331909418106079101562501 is not represented exactly. Will use 0x1.0000000000000p-150.
[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:
- 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:
Floating-point constant 0.00000000000000000000000000000000000000000000070064923216240853546186479164495806564013097093825788587853414194489554134293030074331909418106079101562501f is not represented exactly. Will use 0x1.0000000000000p-149.
[eva] Analyzing a complete application starting at main
@@ -137,11 +137,11 @@
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
- f_ ∈ {-0x0.0000000000000p-1022}
+ f_ ∈ {-0x0.0000000000000p0}
f00 ∈ {0}
f2 ∈ {0x1.8000000000000p1}
f3 ∈ {0x1.8000000000000p1}
- f_0 ∈ [-0x0.0000000000000p-1022 .. 0x0.0000000000000p-1022]
+ f_0 ∈ [-0x0.0000000000000p0 .. 0x0.0000000000000p0]
f13 ∈ [0x1.0000000000000p0 .. 0x1.8000000000000p1]
f26 ∈ [0x1.0000000000000p1 .. 0x1.8000000000000p2]
fic0 ∈ {0}
@@ -151,10 +151,10 @@
fec0 ∈ {0}
fec2 ∈ {0x1.0000000000000p1}
fec4 ∈ {0x1.0000000000000p2}
- m_ ∈ {-0x0.0000000000000p-1022}
+ m_ ∈ {-0x0.0000000000000p0}
m00 ∈ {0}
m2 ∈ {0x1.8000000000000p1}
- m_0 ∈ [-0x0.0000000000000p-1022 .. 0x0.0000000000000p-1022]
+ m_0 ∈ [-0x0.0000000000000p0 .. 0x0.0000000000000p0]
m13 ∈ [0x1.0000000000000p0 .. 0x1.8000000000000p1]
m26 ∈ [0x1.0000000000000p1 .. 0x1.8000000000000p2]
d2 ∈ {0x1.8000000000000p1}
diff --git a/tests/float/oracle/logic.0.res.oracle b/tests/float/oracle/logic.0.res.oracle
index a5db6778fcbd447992f1b8d621519278457e4fc0..a78dc74e8eaac554d264eb78a2b28fffc8e7de2c 100644
--- a/tests/float/oracle/logic.0.res.oracle
+++ b/tests/float/oracle/logic.0.res.oracle
@@ -112,55 +112,46 @@
Called from tests/float/logic.i:118.
[eva] tests/float/logic.i:84:
Frama_C_show_each_eq:
- {-0x0.0000000000000p-1022},
- [-0x0.0000000000000p-1022 .. 0x0.0000000000000p-1022]
+ {-0x0.0000000000000p0}, [-0x0.0000000000000p0 .. 0x0.0000000000000p0]
[eva] tests/float/logic.i:88:
Frama_C_show_each_lt:
- {-0x0.0000000000000p-1022},
- [-0x1.fffffffffffffp1023 .. -0x0.0000000000001p-1022]
+ {-0x0.0000000000000p0}, [-0x1.fffffffffffffp1023 .. -0x0.0000000000001p-1022]
[eva] tests/float/logic.i:92:
Frama_C_show_each_lt:
- {-0x0.0000000000000p-1022},
- [-0x1.fffffffffffffp1023 .. 0x0.0000000000000p-1022]
+ {-0x0.0000000000000p0}, [-0x1.fffffffffffffp1023 .. 0x0.0000000000000p0]
[eva] tests/float/logic.i:96:
Frama_C_show_each_eq_double:
- {-0x0.0000000000000p-1022},
- [-0x0.0000000000000p-1022 .. 0x0.0000000000000p-1022]
+ {-0x0.0000000000000p0}, [-0x0.0000000000000p0 .. 0x0.0000000000000p0]
[eva] tests/float/logic.i:100:
Frama_C_show_each_lt_double:
- {-0x0.0000000000000p-1022},
- [-0x1.fffffffffffffp1023 .. -0x0.0000000000001p-1022]
+ {-0x0.0000000000000p0}, [-0x1.fffffffffffffp1023 .. -0x0.0000000000001p-1022]
[eva] tests/float/logic.i:104:
Frama_C_show_each_le_double:
- {-0x0.0000000000000p-1022},
- [-0x1.fffffffffffffp1023 .. 0x0.0000000000000p-1022]
+ {-0x0.0000000000000p0}, [-0x1.fffffffffffffp1023 .. 0x0.0000000000000p0]
[eva] tests/float/logic.i:108:
Frama_C_show_each_ne_double:
- {-0x0.0000000000000p-1022},
- [-0x1.fffffffffffffp1023 .. 0x1.fffffffffffffp1023]
+ {-0x0.0000000000000p0}, [-0x1.fffffffffffffp1023 .. 0x1.fffffffffffffp1023]
[eva] Recording results for test_comparison_reduction
[eva] Done for function test_comparison_reduction
[eva] computing for function test_comparison_reduction <-
test_builtin_comparisons <- main.
Called from tests/float/logic.i:119.
[eva] tests/float/logic.i:84:
- Frama_C_show_each_eq:
- {0}, [-0x0.0000000000000p-1022 .. 0x0.0000000000000p-1022]
+ Frama_C_show_each_eq: {0}, [-0x0.0000000000000p0 .. 0x0.0000000000000p0]
[eva] tests/float/logic.i:88:
Frama_C_show_each_lt:
{0}, [-0x1.fffffffffffffp1023 .. -0x0.0000000000001p-1022]
[eva] tests/float/logic.i:92:
- Frama_C_show_each_lt:
- {0}, [-0x1.fffffffffffffp1023 .. 0x0.0000000000000p-1022]
+ Frama_C_show_each_lt: {0}, [-0x1.fffffffffffffp1023 .. 0x0.0000000000000p0]
[eva] tests/float/logic.i:96:
Frama_C_show_each_eq_double:
- {0}, [-0x0.0000000000000p-1022 .. 0x0.0000000000000p-1022]
+ {0}, [-0x0.0000000000000p0 .. 0x0.0000000000000p0]
[eva] tests/float/logic.i:100:
Frama_C_show_each_lt_double:
{0}, [-0x1.fffffffffffffp1023 .. -0x0.0000000000001p-1022]
[eva] tests/float/logic.i:104:
Frama_C_show_each_le_double:
- {0}, [-0x1.fffffffffffffp1023 .. 0x0.0000000000000p-1022]
+ {0}, [-0x1.fffffffffffffp1023 .. 0x0.0000000000000p0]
[eva] tests/float/logic.i:108:
Frama_C_show_each_ne_double:
{0}, [-0x1.fffffffffffffp1023 .. 0x1.fffffffffffffp1023]
@@ -228,31 +219,31 @@
Called from tests/float/logic.i:126.
[eva] tests/float/logic.i:84:
Frama_C_show_each_eq:
- [-0x1.4000000000000p3 .. -0x0.0000000000000p-1022],
- [-0x1.4000000000000p3 .. 0x0.0000000000000p-1022]
+ [-0x1.4000000000000p3 .. -0x0.0000000000000p0],
+ [-0x1.4000000000000p3 .. 0x0.0000000000000p0]
[eva] tests/float/logic.i:88:
Frama_C_show_each_lt:
- [-0x1.4000000000000p3 .. -0x0.0000000000000p-1022],
+ [-0x1.4000000000000p3 .. -0x0.0000000000000p0],
[-0x1.fffffffffffffp1023 .. -0x0.0000000000001p-1022]
[eva] tests/float/logic.i:92:
Frama_C_show_each_lt:
- [-0x1.4000000000000p3 .. -0x0.0000000000000p-1022],
- [-0x1.fffffffffffffp1023 .. 0x0.0000000000000p-1022]
+ [-0x1.4000000000000p3 .. -0x0.0000000000000p0],
+ [-0x1.fffffffffffffp1023 .. 0x0.0000000000000p0]
[eva] tests/float/logic.i:96:
Frama_C_show_each_eq_double:
- [-0x1.4000000000000p3 .. -0x0.0000000000000p-1022],
- [-0x1.4000000000000p3 .. 0x0.0000000000000p-1022]
+ [-0x1.4000000000000p3 .. -0x0.0000000000000p0],
+ [-0x1.4000000000000p3 .. 0x0.0000000000000p0]
[eva] tests/float/logic.i:100:
Frama_C_show_each_lt_double:
- [-0x1.4000000000000p3 .. -0x0.0000000000000p-1022],
+ [-0x1.4000000000000p3 .. -0x0.0000000000000p0],
[-0x1.fffffffffffffp1023 .. -0x0.0000000000001p-1022]
[eva] tests/float/logic.i:104:
Frama_C_show_each_le_double:
- [-0x1.4000000000000p3 .. -0x0.0000000000000p-1022],
- [-0x1.fffffffffffffp1023 .. 0x0.0000000000000p-1022]
+ [-0x1.4000000000000p3 .. -0x0.0000000000000p0],
+ [-0x1.fffffffffffffp1023 .. 0x0.0000000000000p0]
[eva] tests/float/logic.i:108:
Frama_C_show_each_ne_double:
- [-0x1.4000000000000p3 .. -0x0.0000000000000p-1022],
+ [-0x1.4000000000000p3 .. -0x0.0000000000000p0],
[-0x1.fffffffffffffp1023 .. 0x1.fffffffffffffp1023]
[eva] Recording results for test_comparison_reduction
[eva] Done for function test_comparison_reduction
@@ -261,31 +252,31 @@
Called from tests/float/logic.i:128.
[eva] tests/float/logic.i:84:
Frama_C_show_each_eq:
- [-0x1.4000000000000p3 .. 0x0.0000000000000p-1022],
- [-0x1.4000000000000p3 .. 0x0.0000000000000p-1022]
+ [-0x1.4000000000000p3 .. 0x0.0000000000000p0],
+ [-0x1.4000000000000p3 .. 0x0.0000000000000p0]
[eva] tests/float/logic.i:88:
Frama_C_show_each_lt:
- [-0x1.4000000000000p3 .. 0x0.0000000000000p-1022],
+ [-0x1.4000000000000p3 .. 0x0.0000000000000p0],
[-0x1.fffffffffffffp1023 .. -0x0.0000000000001p-1022]
[eva] tests/float/logic.i:92:
Frama_C_show_each_lt:
- [-0x1.4000000000000p3 .. 0x0.0000000000000p-1022],
- [-0x1.fffffffffffffp1023 .. 0x0.0000000000000p-1022]
+ [-0x1.4000000000000p3 .. 0x0.0000000000000p0],
+ [-0x1.fffffffffffffp1023 .. 0x0.0000000000000p0]
[eva] tests/float/logic.i:96:
Frama_C_show_each_eq_double:
- [-0x1.4000000000000p3 .. 0x0.0000000000000p-1022],
- [-0x1.4000000000000p3 .. 0x0.0000000000000p-1022]
+ [-0x1.4000000000000p3 .. 0x0.0000000000000p0],
+ [-0x1.4000000000000p3 .. 0x0.0000000000000p0]
[eva] tests/float/logic.i:100:
Frama_C_show_each_lt_double:
- [-0x1.4000000000000p3 .. 0x0.0000000000000p-1022],
+ [-0x1.4000000000000p3 .. 0x0.0000000000000p0],
[-0x1.fffffffffffffp1023 .. -0x0.0000000000001p-1022]
[eva] tests/float/logic.i:104:
Frama_C_show_each_le_double:
- [-0x1.4000000000000p3 .. 0x0.0000000000000p-1022],
- [-0x1.fffffffffffffp1023 .. 0x0.0000000000000p-1022]
+ [-0x1.4000000000000p3 .. 0x0.0000000000000p0],
+ [-0x1.fffffffffffffp1023 .. 0x0.0000000000000p0]
[eva] tests/float/logic.i:108:
Frama_C_show_each_ne_double:
- [-0x1.4000000000000p3 .. 0x0.0000000000000p-1022],
+ [-0x1.4000000000000p3 .. 0x0.0000000000000p0],
[-0x1.fffffffffffffp1023 .. 0x1.fffffffffffffp1023]
[eva] Recording results for test_comparison_reduction
[eva] Done for function test_comparison_reduction
@@ -368,7 +359,7 @@
__retres ∈ {-0x1.bca1b00000000p-1}
[eva:final-states] Values at end of function test_comparison_evaluation:
zero ∈ {0}
- minus_zero ∈ {-0x0.0000000000000p-1022}
+ minus_zero ∈ {-0x0.0000000000000p0}
one ∈ {0x1.0000000000000p0}
higher ∈ [0x1.91eb860000000p1 .. 0x1.9000000000000p3]
middle ∈ [-0x1.91eb860000000p1 .. 0x1.91eb860000000p1]
diff --git a/tests/float/oracle/logic.1.res.oracle b/tests/float/oracle/logic.1.res.oracle
index b96f0877b04afbdaa6c5b4ac5b41541a316de63d..bb6624dbb5c74b65b0b362f284d69594f5b29aa7 100644
--- a/tests/float/oracle/logic.1.res.oracle
+++ b/tests/float/oracle/logic.1.res.oracle
@@ -116,24 +116,22 @@
test_builtin_comparisons <- main.
Called from tests/float/logic.i:118.
[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:
- 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:
- 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:
Frama_C_show_each_eq_double:
- {-0x0.0000000000000p-1022},
- [-0x0.0000000000000p-1022 .. 0x0.0000000000000p-1022]
+ {-0x0.0000000000000p0}, [-0x0.0000000000000p0 .. 0x0.0000000000000p0]
[eva] tests/float/logic.i:100:
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:
Frama_C_show_each_le_double:
- {-0x0.0000000000000p-1022}, [-inf .. 0x0.0000000000000p-1022]
+ {-0x0.0000000000000p0}, [-inf .. 0x0.0000000000000p0]
[eva] tests/float/logic.i:108:
- Frama_C_show_each_ne_double:
- {-0x0.0000000000000p-1022}, [-inf .. inf] ∪ {NaN}
+ Frama_C_show_each_ne_double: {-0x0.0000000000000p0}, [-inf .. inf] ∪ {NaN}
[eva] Recording results for test_comparison_reduction
[eva] Done for function test_comparison_reduction
[eva] computing for function test_comparison_reduction <-
@@ -144,11 +142,11 @@
[eva] tests/float/logic.i:92: Frama_C_show_each_lt: {0}, [-inf .. inf] ∪ {NaN}
[eva] tests/float/logic.i:96:
Frama_C_show_each_eq_double:
- {0}, [-0x0.0000000000000p-1022 .. 0x0.0000000000000p-1022]
+ {0}, [-0x0.0000000000000p0 .. 0x0.0000000000000p0]
[eva] tests/float/logic.i:100:
Frama_C_show_each_lt_double: {0}, [-inf .. -0x0.0000000000001p-1022]
[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:
Frama_C_show_each_ne_double: {0}, [-inf .. inf] ∪ {NaN}
[eva] Recording results for test_comparison_reduction
@@ -208,28 +206,27 @@
Called from tests/float/logic.i:126.
[eva] tests/float/logic.i:84:
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:
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:
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:
Frama_C_show_each_eq_double:
- [-0x1.4000000000000p3 .. -0x0.0000000000000p-1022],
- [-0x1.4000000000000p3 .. 0x0.0000000000000p-1022]
+ [-0x1.4000000000000p3 .. -0x0.0000000000000p0],
+ [-0x1.4000000000000p3 .. 0x0.0000000000000p0]
[eva] tests/float/logic.i:100:
Frama_C_show_each_lt_double:
- [-0x1.4000000000000p3 .. -0x0.0000000000000p-1022],
+ [-0x1.4000000000000p3 .. -0x0.0000000000000p0],
[-inf .. -0x0.0000000000001p-1022]
[eva] tests/float/logic.i:104:
Frama_C_show_each_le_double:
- [-0x1.4000000000000p3 .. -0x0.0000000000000p-1022],
- [-inf .. 0x0.0000000000000p-1022]
+ [-0x1.4000000000000p3 .. -0x0.0000000000000p0], [-inf .. 0x0.0000000000000p0]
[eva] tests/float/logic.i:108:
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] Done for function test_comparison_reduction
[eva] computing for function test_comparison_reduction <-
@@ -237,28 +234,27 @@
Called from tests/float/logic.i:128.
[eva] tests/float/logic.i:84:
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:
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:
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:
Frama_C_show_each_eq_double:
- [-0x1.4000000000000p3 .. 0x0.0000000000000p-1022],
- [-0x1.4000000000000p3 .. 0x0.0000000000000p-1022]
+ [-0x1.4000000000000p3 .. 0x0.0000000000000p0],
+ [-0x1.4000000000000p3 .. 0x0.0000000000000p0]
[eva] tests/float/logic.i:100:
Frama_C_show_each_lt_double:
- [-0x1.4000000000000p3 .. 0x0.0000000000000p-1022],
+ [-0x1.4000000000000p3 .. 0x0.0000000000000p0],
[-inf .. -0x0.0000000000001p-1022]
[eva] tests/float/logic.i:104:
Frama_C_show_each_le_double:
- [-0x1.4000000000000p3 .. 0x0.0000000000000p-1022],
- [-inf .. 0x0.0000000000000p-1022]
+ [-0x1.4000000000000p3 .. 0x0.0000000000000p0], [-inf .. 0x0.0000000000000p0]
[eva] tests/float/logic.i:108:
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] Done for function test_comparison_reduction
[eva] computing for function test_comparison_reduction <-
@@ -368,7 +364,7 @@
__retres ∈ {-0x1.bca1b00000000p-1}
[eva:final-states] Values at end of function test_comparison_evaluation:
zero ∈ {0}
- minus_zero ∈ {-0x0.0000000000000p-1022}
+ minus_zero ∈ {-0x0.0000000000000p0}
one ∈ {0x1.0000000000000p0}
higher ∈ [0x1.91eb860000000p1 .. 0x1.9000000000000p3]
middle ∈ [-0x1.91eb860000000p1 .. 0x1.91eb860000000p1]
diff --git a/tests/float/oracle/nonlin.0.res.oracle b/tests/float/oracle/nonlin.0.res.oracle
index 6d1d4f37afd1253fb605b4b558fb0c6fae3766e5..95c633d605b3c85d119c84dc019c403d42da933d 100644
--- a/tests/float/oracle/nonlin.0.res.oracle
+++ b/tests/float/oracle/nonlin.0.res.oracle
@@ -247,7 +247,7 @@
[eva:final-states] Values at end of function around_zeros:
Frama_C_entropy_source ∈ [--..--]
f1 ∈ {0x1.0000000000000p-149}
- f ∈ [-0x0.0000000000000p-1022 .. 0x1.0000000000000p-149]
+ f ∈ [-0x0.0000000000000p0 .. 0x1.0000000000000p-149]
res ∈ [-0x1.fffffe0000000p127 .. 0x1.fffffe0000000p127]
[eva:final-states] Values at end of function garbled:
a_0 ∈
@@ -257,7 +257,7 @@
[eva:final-states] Values at end of function nonlin_f:
Frama_C_entropy_source ∈ [--..--]
a ∈ [0x1.4000000000000p2 .. 0x1.c000000000000p2]
- b ∈ [-0x0.0000000000000p-1022 .. 0x1.0000000000000p0]
+ b ∈ [-0x0.0000000000000p0 .. 0x1.0000000000000p0]
c ∈ {0x1.c000000000000p2}
r1 ∈ [0x1.4000000000000p2 .. 0x1.2000000000000p3]
r2 ∈ [0x1.4000000000000p2 .. 0x1.c800000000000p2]
@@ -286,7 +286,7 @@
[eva:final-states] Values at end of function main:
Frama_C_entropy_source ∈ [--..--]
a ∈ [0x1.4000000000000p2 .. 0x1.c000000000000p2]
- b ∈ [-0x0.0000000000000p-1022 .. 0x1.0000000000000p0]
+ b ∈ [-0x0.0000000000000p0 .. 0x1.0000000000000p0]
c ∈ {0x1.c000000000000p2}
r1 ∈ [0x1.4000000000000p2 .. 0x1.2000000000000p3]
r2 ∈ [0x1.4000000000000p2 .. 0x1.c800000000000p2]
diff --git a/tests/float/oracle/nonlin.1.res.oracle b/tests/float/oracle/nonlin.1.res.oracle
index ec20b5dbc24d8c34781a2d2cb7e935ebe29ddfaf..f1aa30fd850f5bf88444511a31c4390c0696ade2 100644
--- a/tests/float/oracle/nonlin.1.res.oracle
+++ b/tests/float/oracle/nonlin.1.res.oracle
@@ -270,7 +270,7 @@
[eva:final-states] Values at end of function around_zeros:
Frama_C_entropy_source ∈ [--..--]
f1 ∈ {0x1.0000000000000p-149}
- f ∈ [-0x0.0000000000000p-1022 .. 0x0.0000000000000p-1022]
+ f ∈ [-0x0.0000000000000p0 .. 0x0.0000000000000p0]
res ∈ {-0x1.0000000000000p0}
[eva:final-states] Values at end of function garbled:
a_0 ∈
@@ -280,7 +280,7 @@
[eva:final-states] Values at end of function nonlin_f:
Frama_C_entropy_source ∈ [--..--]
a ∈ [0x1.4000000000000p2 .. 0x1.c000000000000p2]
- b ∈ [-0x0.0000000000000p-1022 .. 0x1.0000000000000p0]
+ b ∈ [-0x0.0000000000000p0 .. 0x1.0000000000000p0]
c ∈ {0x1.c000000000000p2}
r1 ∈ [0x1.4000000000000p2 .. 0x1.cffffffffffffp2]
r2 ∈ [0x1.4000000000000p2 .. 0x1.c0fffffffffffp2]
@@ -288,7 +288,7 @@
[eva:final-states] Values at end of function norm:
v1 ∈ [-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:
Frama_C_entropy_source ∈ [--..--]
i ∈ [-0x1.714fffffffff7p1 .. 0x1.71c0000000003p1]
@@ -309,7 +309,7 @@
[eva:final-states] Values at end of function main:
Frama_C_entropy_source ∈ [--..--]
a ∈ [0x1.4000000000000p2 .. 0x1.c000000000000p2]
- b ∈ [-0x0.0000000000000p-1022 .. 0x1.0000000000000p0]
+ b ∈ [-0x0.0000000000000p0 .. 0x1.0000000000000p0]
c ∈ {0x1.c000000000000p2}
r1 ∈ [0x1.4000000000000p2 .. 0x1.cffffffffffffp2]
r2 ∈ [0x1.4000000000000p2 .. 0x1.c0fffffffffffp2]
diff --git a/tests/float/oracle/nonlin.2.res.oracle b/tests/float/oracle/nonlin.2.res.oracle
index 55f870a84bcdd6c2e6f5c9025399144c0d05e58d..d8f939ec1d88d22950096d4bcd45a9dfe16bc7e4 100644
--- a/tests/float/oracle/nonlin.2.res.oracle
+++ b/tests/float/oracle/nonlin.2.res.oracle
@@ -247,7 +247,7 @@
[eva:final-states] Values at end of function around_zeros:
Frama_C_entropy_source ∈ [--..--]
f1 ∈ {0x1.0000000000000p-149}
- f ∈ [-0x0.0000000000000p-1022 .. 0x1.0000000000000p-149]
+ f ∈ [-0x0.0000000000000p0 .. 0x1.0000000000000p-149]
res ∈ [-0x1.fffffe0000000p127 .. 0x1.fffffe0000000p127]
[eva:final-states] Values at end of function garbled:
a_0 ∈
@@ -257,7 +257,7 @@
[eva:final-states] Values at end of function nonlin_f:
Frama_C_entropy_source ∈ [--..--]
a ∈ [0x1.4000000000000p2 .. 0x1.c000000000000p2]
- b ∈ [-0x0.0000000000000p-1022 .. 0x1.0000000000000p0]
+ b ∈ [-0x0.0000000000000p0 .. 0x1.0000000000000p0]
c ∈ {0x1.c000000000000p2}
r1 ∈ [0x1.4000000000000p2 .. 0x1.2000000000000p3]
r2 ∈ [0x1.4000000000000p2 .. 0x1.c800000000000p2]
@@ -286,7 +286,7 @@
[eva:final-states] Values at end of function main:
Frama_C_entropy_source ∈ [--..--]
a ∈ [0x1.4000000000000p2 .. 0x1.c000000000000p2]
- b ∈ [-0x0.0000000000000p-1022 .. 0x1.0000000000000p0]
+ b ∈ [-0x0.0000000000000p0 .. 0x1.0000000000000p0]
c ∈ {0x1.c000000000000p2}
r1 ∈ [0x1.4000000000000p2 .. 0x1.2000000000000p3]
r2 ∈ [0x1.4000000000000p2 .. 0x1.c800000000000p2]
diff --git a/tests/float/oracle/nonlin.3.res.oracle b/tests/float/oracle/nonlin.3.res.oracle
index 81c915845524d4a3fe60b0bb518b170df0c80389..1a9170be5a49927871fee4b6f676bc4f1856b6aa 100644
--- a/tests/float/oracle/nonlin.3.res.oracle
+++ b/tests/float/oracle/nonlin.3.res.oracle
@@ -270,7 +270,7 @@
[eva:final-states] Values at end of function around_zeros:
Frama_C_entropy_source ∈ [--..--]
f1 ∈ {0x1.0000000000000p-149}
- f ∈ [-0x0.0000000000000p-1022 .. 0x0.0000000000000p-1022]
+ f ∈ [-0x0.0000000000000p0 .. 0x0.0000000000000p0]
res ∈ {-0x1.0000000000000p0}
[eva:final-states] Values at end of function garbled:
a_0 ∈
@@ -280,7 +280,7 @@
[eva:final-states] Values at end of function nonlin_f:
Frama_C_entropy_source ∈ [--..--]
a ∈ [0x1.4000000000000p2 .. 0x1.c000000000000p2]
- b ∈ [-0x0.0000000000000p-1022 .. 0x1.0000000000000p0]
+ b ∈ [-0x0.0000000000000p0 .. 0x1.0000000000000p0]
c ∈ {0x1.c000000000000p2}
r1 ∈ [0x1.4000000000000p2 .. 0x1.cffffe0000000p2]
r2 ∈ [0x1.4000000000000p2 .. 0x1.c0fffe0000000p2]
@@ -288,7 +288,7 @@
[eva:final-states] Values at end of function norm:
v1 ∈ [-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:
Frama_C_entropy_source ∈ [--..--]
i ∈ [-0x1.714fee0000000p1 .. 0x1.71c0040000000p1]
@@ -309,7 +309,7 @@
[eva:final-states] Values at end of function main:
Frama_C_entropy_source ∈ [--..--]
a ∈ [0x1.4000000000000p2 .. 0x1.c000000000000p2]
- b ∈ [-0x0.0000000000000p-1022 .. 0x1.0000000000000p0]
+ b ∈ [-0x0.0000000000000p0 .. 0x1.0000000000000p0]
c ∈ {0x1.c000000000000p2}
r1 ∈ [0x1.4000000000000p2 .. 0x1.cffffe0000000p2]
r2 ∈ [0x1.4000000000000p2 .. 0x1.c0fffe0000000p2]
diff --git a/tests/value/oracle/cond_integer_cast_of_float.res.oracle b/tests/value/oracle/cond_integer_cast_of_float.res.oracle
index 155d172a35dc47fea547d2fc34072173597e0c97..1111e966466fff474fc3a0967b31d1ded39ed23f 100644
--- a/tests/value/oracle/cond_integer_cast_of_float.res.oracle
+++ b/tests/value/oracle/cond_integer_cast_of_float.res.oracle
@@ -152,7 +152,7 @@
[eva] tests/value/cond_integer_cast_of_float.i:17:
Frama_C_show_each_float_: [0x1.0000000000000p1 .. 0x1.0000000000000p3]
[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:
Frama_C_show_each_float_: [0x1.0000000000000p0 .. 0x1.0000000000000p3]
[eva] tests/value/cond_integer_cast_of_float.i:26:
@@ -160,13 +160,13 @@
[eva] tests/value/cond_integer_cast_of_float.i:29:
Frama_C_show_each_double: [0x1.0000000000000p1 .. 0x1.0000000000000p3]
[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:
Frama_C_show_each_double: [0x1.0000000000000p0 .. 0x1.0000000000000p3]
[eva] tests/value/cond_integer_cast_of_float.i:38:
Frama_C_show_each_double: [0x1.8000000000000p1 .. 0x1.fffffffffffffp1]
[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] Done for function main1
[eva] computing for function main2 <- main <- mainbis.