diff --git a/src/plugins/value/engine/analysis.ml b/src/plugins/value/engine/analysis.ml index 5cb98e37e081c78603150f34bbf50b2e184901ba..e27e529fc79c30f7a4e47fd4de05a01b73f8b732 100644 --- a/src/plugins/value/engine/analysis.ml +++ b/src/plugins/value/engine/analysis.ml @@ -173,6 +173,7 @@ let reset_analyzer () = let force_compute () = Ast.compute (); Value_parameters.configure_precision (); + Value_parameters.print_correctness_parameters (); 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 7714801f87bdc613d7a694f723c721172a12bfbf..c382bbeb4fa84305d17057a590e1a54261c07cba 100644 --- a/src/plugins/value/value_parameters.ml +++ b/src/plugins/value/value_parameters.ml @@ -82,6 +82,7 @@ let dkey_incompatible_states = register_category "incompatible-states" let dkey_iterator = register_category "iterator" let dkey_callbacks = register_category "callbacks" let dkey_widening = register_category "widening" +let dkey_correctness = register_category "correctness" let () = let activate dkey = add_debug_keys dkey in @@ -1424,6 +1425,16 @@ let parameters_correctness = let parameters_tuning = Typed_parameter.Set.elements !parameters_tuning +let print_correctness_parameters () = + feedback ~dkey:dkey_correctness + "Parameters affecting the correctness of the analysis:"; + let print param = + let name = param.Typed_parameter.name in + let value = Typed_parameter.get_value param in + printf " %s: %s" name value + in + if is_debug_key_enabled dkey_correctness + then List.iter print parameters_correctness (* diff --git a/src/plugins/value/value_parameters.mli b/src/plugins/value/value_parameters.mli index 0a294b1e8c116567bfb723b1843c173484228d91..80ce2bc8ae723447e24ce59cfa0fe3d82f8f11f8 100644 --- a/src/plugins/value/value_parameters.mli +++ b/src/plugins/value/value_parameters.mli @@ -153,6 +153,8 @@ 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 + (** Debug categories responsible for printing initial and final states of Value. Enabled by default, but can be disabled via the command-line: -value-msg-key="-initial_state,-final_state" *)