diff --git a/src/plugins/value/value_parameters.ml b/src/plugins/value/value_parameters.ml index 494a55fc98f21b9986e5d52116d7f3aacecf67aa..c6027b04ee524ef02df19d3980becc6a53f9a74b 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 f4a45c439725835d976b9b8ddb41bd3e7274fee1..66971b862613b121bd1d5da7a0e8c6d075dda4f0 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 7f1381022516acfaa8fa4bc0e640684d198fd245..a9396f3728820a8d75d1d51a1ec4d0036f266d58 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 48bccfcaa65d61b768eedbdd041f8799e4a8655f..ef5899feb1099f936b7ab7fc5bb6ba878f08fee0 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.