diff --git a/src/plugins/wp/ProverWhy3.ml b/src/plugins/wp/ProverWhy3.ml
index 5bdb372b64d5ed74927ac8e2f192c9e25f21c2f6..7f1b75155612e1354543f1ed4626cb21d41d0424 100644
--- a/src/plugins/wp/ProverWhy3.ml
+++ b/src/plugins/wp/ProverWhy3.ml
@@ -285,10 +285,10 @@ module Literal = struct
let float_literal_from_q ~cnv tau q =
let use_hex = true in
- let f = Q.to_float q in
- let s = Format.asprintf "%a" (Floating_point.pretty_normal ~use_hex) f in
- let s = match cfloat_of_tau tau with Float32 -> s^"F" | Float64 -> s^"D" in
- let _, { Floating_point.f_nearest = f } = Floating_point.parse s in
+ let f = match cfloat_of_tau tau with
+ | Float32 -> Floating_point.round_to_single_precision_float (Q.to_float q)
+ | Float64 -> Q.to_float q
+ in
let s = Format.asprintf "%a" (Floating_point.pretty_normal ~use_hex) f in
let re_float =
Str.regexp "-?0x\\([0-9a-f]+\\).\\([0-9a-f]+\\)?p?\\([+-]?[0-9a-f]+\\)?$"
diff --git a/src/plugins/wp/share/why3/frama_c_wp/cfloat.mlw b/src/plugins/wp/share/why3/frama_c_wp/cfloat.mlw
index 313c048faf677ab9784e4498e11a5365153da627..aaedd4489efc3d61a0113eca8f6e2a3265efe616 100644
--- a/src/plugins/wp/share/why3/frama_c_wp/cfloat.mlw
+++ b/src/plugins/wp/share/why3/frama_c_wp/cfloat.mlw
@@ -30,6 +30,7 @@ theory Cfloat
use ieee_float.RoundingMode as Rounding
use ieee_float.Float32 as F32
use ieee_float.Float64 as F64
+ use ieee_float.FloatConverter as Cnv
use real.RealInfix
(* -------------------------------------------------------------------------- *)
@@ -82,6 +83,12 @@ theory Cfloat
lemma real_0_is_zero_f32: forall f:f32. 0.0 = of_f32 f -> F32.is_zero f
lemma real_0_is_zero_f64: forall f:f64. 0.0 = of_f64 f -> F64.is_zero f
+ (* Conversions *)
+ axiom f32_to_f64:
+ forall f:f32 [to_f64 (of_f32 f)]. to_f64 (of_f32 f) = Cnv.to_float64 Rounding.RNE f
+ axiom f64_to_f32:
+ forall f:f64 [to_f32 (of_f64 f)]. to_f32 (of_f64 f) = Cnv.to_float32 Rounding.RNE f
+
(* Finite Constants *)
predicate finite (x:real) = (is_finite_f32 (to_f32 x)) /\ (is_finite_f64 (to_f64 x))
diff --git a/src/plugins/wp/tests/wp_acsl/float_const.i b/src/plugins/wp/tests/wp_acsl/float_const.i
new file mode 100644
index 0000000000000000000000000000000000000000..9becb069d883cc189ca38aca1ec3a959599de6f3
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/float_const.i
@@ -0,0 +1,25 @@
+/* run.config
+ OPT:-wp-gen -wp-prover=why3 -wp-msg-key=print-generated -kernel-warn-key parser:decimal-float=active
+*/
+/* run.config_qualif
+ OPT:
+*/
+
+void float_convertible(float f){
+ double d = f ;
+ if(f == 0.1f){
+ //@ check f != 0.1 ;
+ //@ check f == (float)0.1 ;
+ //@ check f != (double)0.1 ;
+ //@ check (float) d == f ;
+ }
+}
+void double_convertible(double d){
+ double x = (float) d ;
+ if(d == 0.1){
+ //@ check d != 0.1 ;
+ //@ check d == (double)0.1 ;
+ //@ check d != (float)0.1 ;
+ //@ check x == (float) d ;
+ }
+}
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/float_const.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/float_const.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..36c2f74c36303b6d9ffb3c4b171977fe6cc9e4ed
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle/float_const.res.oracle
@@ -0,0 +1,326 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp_acsl/float_const.i (no preprocessing)
+[kernel:parser:decimal-float] tests/wp_acsl/float_const.i:10: Warning:
+ Floating-point constant 0.1f is not represented exactly. Will use 0x1.99999a0000000p-4.
+[kernel:parser:decimal-float] tests/wp_acsl/float_const.i:19: Warning:
+ Floating-point constant 0.1 is not represented exactly. Will use 0x1.999999999999ap-4.
+[wp] Running WP plugin...
+[wp] Loading driver 'share/wp.driver'
+[wp] Warning: Missing RTE guards
+[wp] 8 goals scheduled
+[wp:print-generated]
+ theory WP
+ (* use why3.BuiltIn.BuiltIn *)
+
+ (* use bool.Bool *)
+
+ (* use int.Int *)
+
+ (* use int.ComputerDivision *)
+
+ (* use real.RealInfix *)
+
+ (* use frama_c_wp.qed.Qed *)
+
+ (* use map.Map *)
+
+ (* use real.Abs *)
+
+ (* use frama_c_wp.cmath.Cmath *)
+
+ (* use real.Square *)
+
+ (* use frama_c_wp.cmath.Square1 *)
+
+ (* use frama_c_wp.cfloat.Cfloat *)
+
+ goal wp_goal :
+ forall f:t.
+ let r = of_f32 (to_f32 (of_f64 f)) in
+ eq_f64 f (0x1.999999999999ap-4:t) -> of_f64 (to_f64 r) = r
+ end
+[wp:print-generated]
+ theory WP1
+ (* use why3.BuiltIn.BuiltIn *)
+
+ (* use bool.Bool *)
+
+ (* use int.Int *)
+
+ (* use int.ComputerDivision *)
+
+ (* use real.RealInfix *)
+
+ (* use frama_c_wp.qed.Qed *)
+
+ (* use map.Map *)
+
+ (* use real.Abs *)
+
+ (* use frama_c_wp.cmath.Cmath *)
+
+ (* use real.Square *)
+
+ (* use frama_c_wp.cmath.Square1 *)
+
+ (* use frama_c_wp.cfloat.Cfloat *)
+
+ goal wp_goal :
+ forall f:t.
+ eq_f64 f (0x1.999999999999ap-4:t) ->
+ not of_f64 f = (13421773.0 / 134217728.0)
+ end
+[wp:print-generated]
+ theory WP2
+ (* use why3.BuiltIn.BuiltIn *)
+
+ (* use bool.Bool *)
+
+ (* use int.Int *)
+
+ (* use int.ComputerDivision *)
+
+ (* use real.RealInfix *)
+
+ (* use frama_c_wp.qed.Qed *)
+
+ (* use map.Map *)
+
+ (* use real.Abs *)
+
+ (* use frama_c_wp.cmath.Cmath *)
+
+ (* use real.Square *)
+
+ (* use frama_c_wp.cmath.Square1 *)
+
+ (* use frama_c_wp.cfloat.Cfloat *)
+
+ goal wp_goal :
+ forall f:t.
+ eq_f64 f (0x1.999999999999ap-4:t) ->
+ of_f64 f = (3602879701896397.0 / 36028797018963968.0)
+ end
+[wp:print-generated]
+ theory WP3
+ (* use why3.BuiltIn.BuiltIn *)
+
+ (* use bool.Bool *)
+
+ (* use int.Int *)
+
+ (* use int.ComputerDivision *)
+
+ (* use real.RealInfix *)
+
+ (* use frama_c_wp.qed.Qed *)
+
+ (* use map.Map *)
+
+ (* use real.Abs *)
+
+ (* use frama_c_wp.cmath.Cmath *)
+
+ (* use real.Square *)
+
+ (* use frama_c_wp.cmath.Square1 *)
+
+ (* use frama_c_wp.cfloat.Cfloat *)
+
+ goal wp_goal :
+ forall f:t.
+ eq_f64 f (0x1.999999999999ap-4:t) -> not of_f64 f = (1.0 / 10.0)
+ end
+[wp:print-generated]
+ theory WP4
+ (* use why3.BuiltIn.BuiltIn *)
+
+ (* use bool.Bool1 *)
+
+ (* use int.Int1 *)
+
+ (* use int.ComputerDivision1 *)
+
+ (* use real.RealInfix1 *)
+
+ (* use frama_c_wp.qed.Qed1 *)
+
+ (* use map.Map1 *)
+
+ (* use real.Abs1 *)
+
+ (* use frama_c_wp.cmath.Cmath1 *)
+
+ (* use real.Square2 *)
+
+ (* use frama_c_wp.cmath.Square3 *)
+
+ (* use frama_c_wp.cfloat.Cfloat1 *)
+
+ goal wp_goal :
+ forall f:t1.
+ let r = of_f321 f in
+ eq_f32 f (0x1.99999a0000000p-4:t1) ->
+ of_f321 (to_f321 (of_f641 (to_f641 r))) = r
+ end
+[wp:print-generated]
+ theory WP5
+ (* use why3.BuiltIn.BuiltIn *)
+
+ (* use bool.Bool1 *)
+
+ (* use int.Int1 *)
+
+ (* use int.ComputerDivision1 *)
+
+ (* use real.RealInfix1 *)
+
+ (* use frama_c_wp.qed.Qed1 *)
+
+ (* use map.Map1 *)
+
+ (* use real.Abs1 *)
+
+ (* use frama_c_wp.cmath.Cmath1 *)
+
+ (* use real.Square2 *)
+
+ (* use frama_c_wp.cmath.Square3 *)
+
+ (* use frama_c_wp.cfloat.Cfloat1 *)
+
+ goal wp_goal :
+ forall f:t1.
+ eq_f32 f (0x1.99999a0000000p-4:t1) ->
+ not of_f321 f = (3602879701896397.0 /' 36028797018963968.0)
+ end
+[wp:print-generated]
+ theory WP6
+ (* use why3.BuiltIn.BuiltIn *)
+
+ (* use bool.Bool1 *)
+
+ (* use int.Int1 *)
+
+ (* use int.ComputerDivision1 *)
+
+ (* use real.RealInfix1 *)
+
+ (* use frama_c_wp.qed.Qed1 *)
+
+ (* use map.Map1 *)
+
+ (* use real.Abs1 *)
+
+ (* use frama_c_wp.cmath.Cmath1 *)
+
+ (* use real.Square2 *)
+
+ (* use frama_c_wp.cmath.Square3 *)
+
+ (* use frama_c_wp.cfloat.Cfloat1 *)
+
+ goal wp_goal :
+ forall f:t1.
+ eq_f32 f (0x1.99999a0000000p-4:t1) ->
+ of_f321 f = (13421773.0 /' 134217728.0)
+ end
+[wp:print-generated]
+ theory WP7
+ (* use why3.BuiltIn.BuiltIn *)
+
+ (* use bool.Bool1 *)
+
+ (* use int.Int1 *)
+
+ (* use int.ComputerDivision1 *)
+
+ (* use real.RealInfix1 *)
+
+ (* use frama_c_wp.qed.Qed1 *)
+
+ (* use map.Map1 *)
+
+ (* use real.Abs1 *)
+
+ (* use frama_c_wp.cmath.Cmath1 *)
+
+ (* use real.Square2 *)
+
+ (* use frama_c_wp.cmath.Square3 *)
+
+ (* use frama_c_wp.cfloat.Cfloat1 *)
+
+ goal wp_goal :
+ forall f:t1.
+ eq_f32 f (0x1.99999a0000000p-4:t1) -> not of_f321 f = (1.0 /' 10.0)
+ end
+[wp] 8 goals generated
+------------------------------------------------------------
+ Function double_convertible
+------------------------------------------------------------
+
+Goal Check (file tests/wp_acsl/float_const.i, line 20):
+Assume {
+ (* Then *)
+ Have: eq_f64(d, to_f64((3602879701896397.0/36028797018963968))).
+}
+Prove: of_f64(d) != (1.0/10).
+
+------------------------------------------------------------
+
+Goal Check (file tests/wp_acsl/float_const.i, line 21):
+Assume {
+ (* Then *)
+ Have: eq_f64(d, to_f64((3602879701896397.0/36028797018963968))).
+}
+Prove: of_f64(d) = (3602879701896397.0/36028797018963968).
+
+------------------------------------------------------------
+
+Goal Check (file tests/wp_acsl/float_const.i, line 22):
+Assume {
+ (* Then *)
+ Have: eq_f64(d, to_f64((3602879701896397.0/36028797018963968))).
+}
+Prove: of_f64(d) != (13421773.0/134217728).
+
+------------------------------------------------------------
+
+Goal Check (file tests/wp_acsl/float_const.i, line 23):
+Let r = of_f32(to_f32(of_f64(d))).
+Assume {
+ (* Then *)
+ Have: eq_f64(d, to_f64((3602879701896397.0/36028797018963968))).
+}
+Prove: of_f64(to_f64(r)) = r.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function float_convertible
+------------------------------------------------------------
+
+Goal Check (file tests/wp_acsl/float_const.i, line 11):
+Assume { (* Then *) Have: eq_f32(f, to_f32((13421773.0/134217728))). }
+Prove: of_f32(f) != (1.0/10).
+
+------------------------------------------------------------
+
+Goal Check (file tests/wp_acsl/float_const.i, line 12):
+Assume { (* Then *) Have: eq_f32(f, to_f32((13421773.0/134217728))). }
+Prove: of_f32(f) = (13421773.0/134217728).
+
+------------------------------------------------------------
+
+Goal Check (file tests/wp_acsl/float_const.i, line 13):
+Assume { (* Then *) Have: eq_f32(f, to_f32((13421773.0/134217728))). }
+Prove: of_f32(f) != (3602879701896397.0/36028797018963968).
+
+------------------------------------------------------------
+
+Goal Check (file tests/wp_acsl/float_const.i, line 14):
+Let r = of_f32(f).
+Assume { (* Then *) Have: eq_f32(f, to_f32((13421773.0/134217728))). }
+Prove: of_f32(to_f32(of_f64(to_f64(r)))) = r.
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.0.res.oracle
index d94b1a0dbd8aa0ee3398624d9296661efe681123..cb949a9f9545c5163da4efda55c2ac57205e9b0b 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.0.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.0.res.oracle
@@ -5,7 +5,7 @@
[wp] Warning: Missing RTE guards
[wp] 19 goals scheduled
[wp] [Alt-Ergo] Goal typed_lemma_finite_32_64 : Valid
-[wp] [Alt-Ergo] Goal typed_lemma_finite_32_64_real : Unsuccess
+[wp] [Alt-Ergo] Goal typed_lemma_finite_32_64_real : Valid
[wp] [Alt-Ergo] Goal typed_lemma_test_double_compare : Valid
[wp] [Alt-Ergo] Goal typed_lemma_test_double_compare_greater : Valid
[wp] [Alt-Ergo] Goal typed_lemma_test_float_compare : Valid
@@ -23,12 +23,12 @@
[wp] [Alt-Ergo] Goal typed_cmp_ff_ensures_REL2 : Valid
[wp] [Qed] Goal typed_cmp_fnan_ensures_POS : Valid
[wp] [Qed] Goal typed_cmp_fnan_ensures_NEG : Valid
-[wp] Proved goals: 18 / 19
+[wp] Proved goals: 19 / 19
Qed: 2
- Alt-Ergo: 16 (unsuccess: 1)
+ Alt-Ergo: 17
------------------------------------------------------------
Axiomatics WP Alt-Ergo Total Success
- Lemma - 5 6 83.3%
+ Lemma - 6 6 100%
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
cmp_ff - 3 3 100%
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_const.0.session/cache/211e52458be3c1ae451dfd1d012b443d.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_const.0.session/cache/211e52458be3c1ae451dfd1d012b443d.json
new file mode 100644
index 0000000000000000000000000000000000000000..74f5bb38c308ea0290053e5f8b87e1a39cc3d4a4
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_const.0.session/cache/211e52458be3c1ae451dfd1d012b443d.json
@@ -0,0 +1,2 @@
+{ "prover": "why3:Alt-Ergo,2.0.0", "verdict": "valid", "time": 0.4341,
+ "steps": 1458 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_const.0.session/cache/3744b87afb2193c88857aec75c88378c.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_const.0.session/cache/3744b87afb2193c88857aec75c88378c.json
new file mode 100644
index 0000000000000000000000000000000000000000..3f3afe181dbf9d2f8bd719d171385dde594f74b4
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_const.0.session/cache/3744b87afb2193c88857aec75c88378c.json
@@ -0,0 +1,2 @@
+{ "prover": "why3:Alt-Ergo,2.0.0", "verdict": "valid", "time": 0.0888,
+ "steps": 332 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_const.0.session/cache/52e0b6c21b84e63c174bec2662584b59.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_const.0.session/cache/52e0b6c21b84e63c174bec2662584b59.json
new file mode 100644
index 0000000000000000000000000000000000000000..bd1857637f18c522c93b33462951b204dca3619f
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_const.0.session/cache/52e0b6c21b84e63c174bec2662584b59.json
@@ -0,0 +1,2 @@
+{ "prover": "why3:Alt-Ergo,2.0.0", "verdict": "valid", "time": 0.2926,
+ "steps": 1145 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_const.0.session/cache/5d05945c4e22b2861b15d558fb83c6e1.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_const.0.session/cache/5d05945c4e22b2861b15d558fb83c6e1.json
new file mode 100644
index 0000000000000000000000000000000000000000..ba30e6254772d7d12b8dac51ce7c7241fad858b1
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_const.0.session/cache/5d05945c4e22b2861b15d558fb83c6e1.json
@@ -0,0 +1,2 @@
+{ "prover": "why3:Alt-Ergo,2.0.0", "verdict": "valid", "time": 0.1586,
+ "steps": 596 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_const.0.session/cache/86231af23e1064da708992cd22fcc6cd.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_const.0.session/cache/86231af23e1064da708992cd22fcc6cd.json
new file mode 100644
index 0000000000000000000000000000000000000000..b614d74d7813fb556ab95e0d42d5381538c9b60a
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_const.0.session/cache/86231af23e1064da708992cd22fcc6cd.json
@@ -0,0 +1,2 @@
+{ "prover": "why3:Alt-Ergo,2.0.0", "verdict": "valid", "time": 0.0916,
+ "steps": 332 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_const.0.session/cache/9c06dc676f02ccbf93885782c64aa8c0.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_const.0.session/cache/9c06dc676f02ccbf93885782c64aa8c0.json
new file mode 100644
index 0000000000000000000000000000000000000000..b3c09fcfc35fed533c6bbb0dccdf31873db923e9
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_const.0.session/cache/9c06dc676f02ccbf93885782c64aa8c0.json
@@ -0,0 +1,2 @@
+{ "prover": "why3:Alt-Ergo,2.0.0", "verdict": "valid", "time": 0.1483,
+ "steps": 596 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_const.0.session/cache/addd047e7326afb3baae18e98392f6ad.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_const.0.session/cache/addd047e7326afb3baae18e98392f6ad.json
new file mode 100644
index 0000000000000000000000000000000000000000..fab86abb6f448b87b768b06097dcb942ab14f420
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_const.0.session/cache/addd047e7326afb3baae18e98392f6ad.json
@@ -0,0 +1,2 @@
+{ "prover": "why3:Alt-Ergo,2.0.0", "verdict": "valid", "time": 0.1022,
+ "steps": 332 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_const.0.session/cache/af03277f3ce7d723e9695176099b9946.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_const.0.session/cache/af03277f3ce7d723e9695176099b9946.json
new file mode 100644
index 0000000000000000000000000000000000000000..6c9b90bb8ecfc3f82771bf26bc7110423141ab6b
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_const.0.session/cache/af03277f3ce7d723e9695176099b9946.json
@@ -0,0 +1,2 @@
+{ "prover": "why3:Alt-Ergo,2.0.0", "verdict": "valid", "time": 0.0908,
+ "steps": 332 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_const.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_const.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..bc8717807fd0d5bfde96f27734717207d76c39db
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_const.res.oracle
@@ -0,0 +1,25 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp_acsl/float_const.i (no preprocessing)
+[kernel:parser:decimal-float] tests/wp_acsl/float_const.i:10: Warning:
+ Floating-point constant 0.1f is not represented exactly. Will use 0x1.99999a0000000p-4.
+ (warn-once: no further messages from category 'parser:decimal-float' will be emitted)
+[wp] Running WP plugin...
+[wp] Loading driver 'share/wp.driver'
+[wp] Warning: Missing RTE guards
+[wp] 8 goals scheduled
+[wp] [Alt-Ergo] Goal typed_double_convertible_check : Valid
+[wp] [Alt-Ergo] Goal typed_double_convertible_check_2 : Valid
+[wp] [Alt-Ergo] Goal typed_double_convertible_check_3 : Valid
+[wp] [Alt-Ergo] Goal typed_double_convertible_check_4 : Valid
+[wp] [Alt-Ergo] Goal typed_float_convertible_check : Valid
+[wp] [Alt-Ergo] Goal typed_float_convertible_check_2 : Valid
+[wp] [Alt-Ergo] Goal typed_float_convertible_check_3 : Valid
+[wp] [Alt-Ergo] Goal typed_float_convertible_check_4 : Valid
+[wp] Proved goals: 8 / 8
+ Qed: 0
+ Alt-Ergo: 8
+------------------------------------------------------------
+ Functions WP Alt-Ergo Total Success
+ float_convertible - 4 4 100%
+ double_convertible - 4 4 100%
+------------------------------------------------------------