diff --git a/src/plugins/value/value_parameters.ml b/src/plugins/value/value_parameters.ml index 00aa3166f88de075b0042ed0a7a5cccd34807ebd..c1a44a5949f45fbb30df7eb57e360f70bc44e22d 100644 --- a/src/plugins/value/value_parameters.ml +++ b/src/plugins/value/value_parameters.ml @@ -495,10 +495,12 @@ module WarnCopyIndeterminate = (struct let option_name = "-eva-warn-copy-indeterminate" let arg_name = "f | @all" - let help = "Warn when a statement of the specified functions copies a \ - value that may be indeterminate (uninitialized or containing \ - escaping address). Set by default; can be deactivated for \ - function 'f' by '=-f', or for all functions by '=-@all'." + let help = + "Warn when a statement copies a value that may be indeterminate \ + (uninitialized, containing an escaping address, or infinite/NaN \ + floating-point value). \ + Set by default; can be deactivated for function 'f' by '=-f', \ + or for all functions by '=-@all'." end) let () = add_correctness_dep WarnCopyIndeterminate.parameter let () = WarnCopyIndeterminate.Category.(set_default (all ()))