From f913345ae069ef6cbcb15f32d484cdccb03f30d6 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Wed, 7 Apr 2021 16:36:50 +0200
Subject: [PATCH] [Eva] Deprecates option -eva-all-rounding-modes-constants.

---
 src/plugins/value/value_parameters.ml  | 30 +++++++++++++++-----------
 tests/float/oracle/const3.1.res.oracle |  2 ++
 tests/float/oracle/const4.1.res.oracle |  2 ++
 tests/float/oracle/dr.2.res.oracle     |  2 ++
 4 files changed, 24 insertions(+), 12 deletions(-)

diff --git a/src/plugins/value/value_parameters.ml b/src/plugins/value/value_parameters.ml
index 494a55fc98f..c6027b04ee5 100644
--- a/src/plugins/value/value_parameters.ml
+++ b/src/plugins/value/value_parameters.ml
@@ -459,17 +459,6 @@ let () = add_precision_dep BitwiseOffsmStorage.parameter
 (* --- Non-standard alarms                                               --- *)
 (* ------------------------------------------------------------------------- *)
 
-let () = Parameter_customize.set_group alarms
-module AllRoundingModesConstants =
-  False
-    (struct
-      let option_name = "-eva-all-rounding-modes-constants"
-      let help = "Take into account the possibility of constants not being \
-                  converted to the nearest representable value, \
-                  or being converted to higher precision"
-    end)
-let () = add_correctness_dep AllRoundingModesConstants.parameter
-
 let () = Parameter_customize.set_group alarms
 module UndefinedPointerComparisonPropagateAll =
   False
@@ -1283,9 +1272,26 @@ let () = MallocLevel.set_range 0 max_int
 let () = add_precision_dep MallocLevel.parameter
 
 (* -------------------------------------------------------------------------- *)
-(* --- Deprecated aliases                                                 --- *)
+(* --- Deprecated options and aliases                                     --- *)
 (* -------------------------------------------------------------------------- *)
 
+let () = Parameter_customize.set_group alarms
+let () = Parameter_customize.is_invisible ()
+module AllRoundingModesConstants =
+  False
+    (struct
+      let option_name = "-eva-all-rounding-modes-constants"
+      let help = "Deprecated. Take into account the possibility of constants \
+                  not being converted to the nearest representable value, \
+                  or being converted to higher precision"
+    end)
+let () = add_correctness_dep AllRoundingModesConstants.parameter
+let () =
+  AllRoundingModesConstants.add_set_hook
+    (fun _old _new ->
+       warning "Option -eva-all-rounding-modes-constants is now deprecated.@ \
+                Please contact us if you need it.")
+
 let deprecated_aliases : ((module Parameter_sig.S) * string) list =
   [ (module SemanticUnrollingLevel), "-slevel"
   ; (module SlevelFunction), "-slevel-function"
diff --git a/tests/float/oracle/const3.1.res.oracle b/tests/float/oracle/const3.1.res.oracle
index f4a45c43972..66971b86261 100644
--- a/tests/float/oracle/const3.1.res.oracle
+++ b/tests/float/oracle/const3.1.res.oracle
@@ -1,3 +1,5 @@
+[eva] Warning: Option -eva-all-rounding-modes-constants is now deprecated.
+  Please contact us if you need it.
 [kernel] Parsing tests/float/const3.i (no preprocessing)
 [kernel:parser:decimal-float] tests/float/const3.i:6: Warning: 
   Floating-point constant 1e-40f is not represented exactly. Will use 0x1.16c2000000000p-133.
diff --git a/tests/float/oracle/const4.1.res.oracle b/tests/float/oracle/const4.1.res.oracle
index 7f138102251..a9396f37288 100644
--- a/tests/float/oracle/const4.1.res.oracle
+++ b/tests/float/oracle/const4.1.res.oracle
@@ -1,3 +1,5 @@
+[eva] Warning: Option -eva-all-rounding-modes-constants is now deprecated.
+  Please contact us if you need it.
 [kernel] Parsing tests/float/const4.i (no preprocessing)
 [kernel:parser:decimal-float] tests/float/const4.i:6: Warning: 
   Floating-point constant 3.4e38f is not represented exactly. Will use 0x1.ff933c0000000p127.
diff --git a/tests/float/oracle/dr.2.res.oracle b/tests/float/oracle/dr.2.res.oracle
index 48bccfcaa65..ef5899feb10 100644
--- a/tests/float/oracle/dr.2.res.oracle
+++ b/tests/float/oracle/dr.2.res.oracle
@@ -1,3 +1,5 @@
+[eva] Warning: Option -eva-all-rounding-modes-constants is now deprecated.
+  Please contact us if you need it.
 [kernel] Parsing tests/float/dr.i (no preprocessing)
 [kernel:parser:decimal-float] tests/float/dr.i:7: Warning: 
   Floating-point constant 100e30f is not represented exactly. Will use 0x1.3b8b5c0000000p106.
-- 
GitLab