Merge branch 'fix/eva/deprecate-option' into 'master'

[Eva] Deprecates option -all-rounding-modes-constant.

See merge request frama-c/frama-c!2986

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"

tests/float/oracle/const3.1.res.oracle

+[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.

tests/float/oracle/const4.1.res.oracle

+[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.

tests/float/oracle/dr.2.res.oracle

+[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.