From 3ff289daaf48d8b410eca190bdc5e4e8978a97a9 Mon Sep 17 00:00:00 2001
From: Valentin Perrelle <valentin.perrelle@cea.fr>
Date: Tue, 30 Nov 2021 18:16:00 +0100
Subject: [PATCH] [Eva] Simplify the usage of Abstraction.dynamic_register
---
src/plugins/value/engine/abstractions.ml | 16 +++++++++++-----
src/plugins/value/engine/abstractions.mli | 3 ++-
2 files changed, 13 insertions(+), 6 deletions(-)
diff --git a/src/plugins/value/engine/abstractions.ml b/src/plugins/value/engine/abstractions.ml
index ac5b7613dc7..daa7f30ed17 100644
--- a/src/plugins/value/engine/abstractions.ml
+++ b/src/plugins/value/engine/abstractions.ml
@@ -74,16 +74,22 @@ module Config = struct
let abstractions = ref []
let dynamic_abstractions = ref []
- let register ~name ~descr ?(experimental=false) ?(priority=0) abstraction =
+ let register_domain_option ~name ~experimental ~descr =
let descr = if experimental then "Experimental. " ^ descr else descr in
- Value_parameters.register_domain ~name ~descr;
+ Value_parameters.register_domain ~name ~descr
+
+ let register ~name ~descr ?(experimental=false) ?(priority=0) abstraction =
+ register_domain_option ~name ~experimental ~descr;
let flag = Flag { name; experimental; priority; abstraction } in
abstractions := flag :: !abstractions;
flag
- let dynamic_register ~name ~descr make =
- Value_parameters.register_domain ~name ~descr;
- dynamic_abstractions := (name, make) :: !dynamic_abstractions
+ let dynamic_register ~name ~descr ?(experimental=false) ?(priority=0) make =
+ register_domain_option ~name ~experimental ~descr;
+ let make' () : flag =
+ Flag { name; experimental; priority; abstraction = make () }
+ in
+ dynamic_abstractions := (name,make') :: !dynamic_abstractions
let configure () =
let add_main_mode mode =
diff --git a/src/plugins/value/engine/abstractions.mli b/src/plugins/value/engine/abstractions.mli
index f5592ba0d47..86d09020a75 100644
--- a/src/plugins/value/engine/abstractions.mli
+++ b/src/plugins/value/engine/abstractions.mli
@@ -94,7 +94,8 @@ val register:
the last argument when starting an analysis, if the -eva-domains option
has been set to [name]. See function {!register} for more details. *)
val dynamic_register:
- name:string -> descr:string -> (unit -> flag) -> unit
+ name:string -> descr:string -> ?experimental:bool -> ?priority:int ->
+ (unit -> 'v abstraction) -> unit
(** Reduced product between two value abstractions, identified by their keys. *)
type ('a, 'b) value_reduced_product =
--
GitLab