From 429837b66e4e2d4b1afabaad9e4481256e745877 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Tue, 1 Sep 2020 08:51:40 +0200
Subject: [PATCH] [Eva] Optionally prints the correctness parameters of an
analysis.
---
src/plugins/value/engine/analysis.ml | 1 +
src/plugins/value/value_parameters.ml | 11 +++++++++++
src/plugins/value/value_parameters.mli | 2 ++
3 files changed, 14 insertions(+)
diff --git a/src/plugins/value/engine/analysis.ml b/src/plugins/value/engine/analysis.ml
index 5cb98e37e08..e27e529fc79 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 7714801f87b..c382bbeb4fa 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 0a294b1e8c1..80ce2bc8ae7 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" *)
--
GitLab