From a5ed19d03f7dd29c2e67910254afd2afc8cfc429 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Thu, 26 Mar 2020 10:53:55 +0100
Subject: [PATCH] [wp] Adds missing 'round' functions to Cfloat MLW

---
 src/plugins/wp/share/why3/frama_c_wp/cfloat.mlw | 13 +++++++++++++
 1 file changed, 13 insertions(+)

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 aaedd4489ef..3cfc3d7f07f 100644
--- a/src/plugins/wp/share/why3/frama_c_wp/cfloat.mlw
+++ b/src/plugins/wp/share/why3/frama_c_wp/cfloat.mlw
@@ -76,6 +76,19 @@ theory Cfloat
   axiom to_f64_minus_infinity: forall x. x <. -. F64.max_real -> is_negative_infinite_f64 (to_f64 x)
   axiom to_f64_plus_infinity: forall x. x >. F64.max_real -> is_positive_infinite_f64 (to_f64 x)
 
+  (* Note: This is OK as we have in Why3 ieee_float:
+
+     axiom Round_idempotent :
+       forall m1 m2:mode, x:real. round m1 (round m2 x) = round m2 x
+
+     So we can round RNE (to_f32/64 behavior) after any rounding.
+  *)
+  function round_float (m: Rounding.mode) (r: real) : f32 =
+    to_f32 (F32.round m r)
+
+  function round_double (m: Rounding.mode) (r: real) : f64 =
+    to_f64 (F64.round m r)
+
   (* Take care of +0/-0 *)
   axiom is_zero_to_f32_zero: F32.is_zero (to_f32 0.0)
   axiom is_zero_to_f64_zero: F64.is_zero (to_f64 0.0)
-- 
GitLab