From 5f00774bc1b1d226a426cfb2a8f6358018dd407c Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Thu, 26 Mar 2020 10:54:27 +0100
Subject: [PATCH] [wp] Updates float drivers to match Cfloat MLW

---
 src/plugins/wp/share/wp.driver | 16 ++++++++--------
 1 file changed, 8 insertions(+), 8 deletions(-)

diff --git a/src/plugins/wp/share/wp.driver b/src/plugins/wp/share/wp.driver
index a45458db4a8..2fb2f16fed1 100644
--- a/src/plugins/wp/share/wp.driver
+++ b/src/plugins/wp/share/wp.driver
@@ -96,12 +96,12 @@ coq.file += "coqwp:real/Abs.v";
 coq.file += "coqwp/Cfloat.v";
 why3.import += "frama_c_wp.cfloat.Cfloat";
 altergo.file += "ergo/Cfloat.mlw";
-type "rounding_mode"   = "rounding_mode";
-ctor "\\Up"()            = "Up";
-ctor "\\Down"()          = "Down";
-ctor "\\ToZero"()        = "ToZero";
-ctor "\\NearestAway"()   = "NearestTiesToAway";
-ctor "\\NearestEven"()   = "NearestTiesToEven";
+type "rounding_mode"   = "Rounding.mode";
+ctor "\\Up"()          = "Rounding.RTP";
+ctor "\\Down"()        = "Rounding.RTN";
+ctor "\\ToZero"()      = "Rounding.RTZ";
+ctor "\\NearestAway"() = "Rounding.RNA";
+ctor "\\NearestEven"() = "Rounding.RNE";
 predicate "\\is_finite"(float32) = "is_finite_f32";
 predicate "\\is_finite"(float64) = "is_finite_f64";
 predicate "\\is_NaN"(float32) = "is_NaN_f32";
@@ -112,8 +112,8 @@ predicate "\\is_plus_infinity"(float32) = "is_positive_infinite_f32";
 predicate "\\is_plus_infinity"(float64) = "is_positive_infinite_f64";
 predicate "\\is_minus_infinity"(float32) = "is_negative_infinite_f32";
 predicate "\\is_minus_infinity"(float64) = "is_negative_infinite_f64";
-logic bool "\\round_float"(rounding_mode,real) = "round_float";
-logic bool "\\round_double"(rounding_mode,real) = "round_double";
+logic float32 "\\round_float"(rounding_mode,real) = "round_float";
+logic float64 "\\round_double"(rounding_mode,real) = "round_double";
 
 library vset:
 type set = "set";
-- 
GitLab