From be084e5b069af163fd5d6716daf40e9ac83f9347 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Wed, 18 Mar 2020 10:19:08 +0100
Subject: [PATCH] [Eva] Engine: do not reset the analyzer when a domain
parameter is changed.
---
src/plugins/value/engine/analysis.ml | 11 +----------
src/plugins/value/value_parameters.ml | 7 -------
src/plugins/value/value_parameters.mli | 1 -
3 files changed, 1 insertion(+), 18 deletions(-)
diff --git a/src/plugins/value/engine/analysis.ml b/src/plugins/value/engine/analysis.ml
index 757510704f6..06c72bf5099 100644
--- a/src/plugins/value/engine/analysis.ml
+++ b/src/plugins/value/engine/analysis.ml
@@ -165,17 +165,8 @@ let force_compute () =
let module Analyzer = (val snd !ref_analyzer) in
Analyzer.compute_from_entry_point ~lib_entry kf
-let set_hook_on_parameter parameter =
- let open Typed_parameter in
- match parameter.accessor with
- | Bool (accessor, _) -> accessor.add_set_hook (fun _ _ -> reset_analyzer ())
- | Int (accessor, _) -> accessor.add_set_hook (fun _ _ -> reset_analyzer ())
- | String (accessor, _) -> accessor.add_set_hook (fun _ _ -> reset_analyzer ())
-
-(* Resets the Analyzer whenever an abstraction parameter or the current project
- is changed. This maintains the analyzer consistent with the Eva parameters. *)
+(* Resets the Analyzer when the current project is changed. *)
let () =
- List.iter set_hook_on_parameter Value_parameters.parameters_abstractions;
Project.register_after_set_current_hook
~user_only:true (fun _ -> reset_analyzer ());
Project.register_after_global_load_hook reset_analyzer
diff --git a/src/plugins/value/value_parameters.ml b/src/plugins/value/value_parameters.ml
index bbe2cb24f8b..597997dccc6 100644
--- a/src/plugins/value/value_parameters.ml
+++ b/src/plugins/value/value_parameters.ml
@@ -234,11 +234,6 @@ module DomainsFunction =
end)
let () = add_precision_dep DomainsFunction.parameter
-(* Set of parameters defining the abstractions used in an Eva analysis. *)
-let parameters_abstractions =
- ref (Typed_parameter.Set.of_list
- [Domains.parameter; DomainsFunction.parameter])
-
let () = Parameter_customize.set_group domains
module EqualityCall =
@@ -1547,8 +1542,6 @@ let parameters_correctness =
Typed_parameter.Set.elements !parameters_correctness
let parameters_tuning =
Typed_parameter.Set.elements !parameters_tuning
-let parameters_abstractions =
- Typed_parameter.Set.elements !parameters_abstractions
diff --git a/src/plugins/value/value_parameters.mli b/src/plugins/value/value_parameters.mli
index 828113a3c87..b31c526f864 100644
--- a/src/plugins/value/value_parameters.mli
+++ b/src/plugins/value/value_parameters.mli
@@ -163,7 +163,6 @@ val configure_precision: unit -> unit
val parameters_correctness: Typed_parameter.t list
val parameters_tuning: Typed_parameter.t list
-val parameters_abstractions: Typed_parameter.t list
(** Debug categories responsible for printing initial and final states of Value.
Enabled by default, but can be disabled via the command-line:
--
GitLab