diff --git a/src/plugins/value/engine/analysis.ml b/src/plugins/value/engine/analysis.ml index e27e529fc79c30f7a4e47fd4de05a01b73f8b732..a3ed9f672096cdb9785e499c10d279421e0e6132 100644 --- a/src/plugins/value/engine/analysis.ml +++ b/src/plugins/value/engine/analysis.ml @@ -173,7 +173,7 @@ let reset_analyzer () = let force_compute () = Ast.compute (); Value_parameters.configure_precision (); - Value_parameters.print_correctness_parameters (); + Value_parameters.print_configuration (); let kf, lib_entry = Globals.entry_point () in reset_analyzer (); let module Analyzer = (val snd !ref_analyzer) in diff --git a/src/plugins/value/value_parameters.ml b/src/plugins/value/value_parameters.ml index c382bbeb4fa84305d17057a590e1a54261c07cba..70dec40e568002f72789954908a55046bb614650 100644 --- a/src/plugins/value/value_parameters.ml +++ b/src/plugins/value/value_parameters.ml @@ -61,13 +61,15 @@ let add_precision_dep p = let () = List.iter add_correctness_dep kernel_parameters_correctness -include Plugin.Register +module Eva = + Plugin.Register (struct let name = "Eva" let shortname = "eva" let help = "automatically computes variation domains for the variables of the program" end) +include Eva let () = Help.add_aliases ~visible:false [ "-value-h"; "-val-h" ] let () = add_plugin_output_aliases ~visible:false ~deprecated:true [ "value" ] @@ -1433,8 +1435,29 @@ let print_correctness_parameters () = let value = Typed_parameter.get_value param in printf " %s: %s" name value in + List.iter print parameters_correctness + +let print_warning_status name (module Plugin: Log.Messages) = + let warning_categories = Plugin.get_all_warn_categories_status () in + let is_active = function + | Log.Winactive | Wfeedback_once | Wfeedback -> false + | Wonce | Wactive | Werror_once | Werror | Wabort -> true + in + let is_enabled (_key, status) = is_active status in + let enabled, disabled = List.partition is_enabled warning_categories in + let pp_categories = Pretty_utils.pp_list ~sep:",@ " Plugin.pp_warn_category in + feedback ~dkey:dkey_correctness "%s warning categories:" name; + printf " Enabled: @[%a@]" pp_categories (List.map fst enabled); + printf " Disabled: @[%a@]" pp_categories (List.map fst disabled) + +let print_configuration () = if is_debug_key_enabled dkey_correctness - then List.iter print parameters_correctness + then + begin + print_correctness_parameters (); + print_warning_status "Kernel" (module Kernel); + print_warning_status "Eva" (module Eva); + end (* diff --git a/src/plugins/value/value_parameters.mli b/src/plugins/value/value_parameters.mli index 80ce2bc8ae723447e24ce59cfa0fe3d82f8f11f8..f9c23f8defb4b0ccc2f31cf66c9cc1831859fb18 100644 --- a/src/plugins/value/value_parameters.mli +++ b/src/plugins/value/value_parameters.mli @@ -153,7 +153,7 @@ val configure_precision: unit -> unit val parameters_correctness: Typed_parameter.t list val parameters_tuning: Typed_parameter.t list -val print_correctness_parameters: unit -> unit +val print_configuration: unit -> unit (** Debug categories responsible for printing initial and final states of Value. Enabled by default, but can be disabled via the command-line: