From 62c282b68cd59bd332cd2f5a10c394edad7e4d68 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Thu, 9 Apr 2020 08:53:57 +0200
Subject: [PATCH] [Eva] Allows registering a dynamic abstraction with several
possible values.
The function given to [dynamic_register] builds directly the flag instead of
only the abstraction.
---
src/plugins/value/engine/abstractions.ml | 23 ++++++-----------------
src/plugins/value/engine/abstractions.mli | 3 +--
2 files changed, 7 insertions(+), 19 deletions(-)
diff --git a/src/plugins/value/engine/abstractions.ml b/src/plugins/value/engine/abstractions.ml
index 5f568596c56..9e18ff813ba 100644
--- a/src/plugins/value/engine/abstractions.ml
+++ b/src/plugins/value/engine/abstractions.ml
@@ -71,10 +71,8 @@ module Config = struct
let mem (Flag domain) =
exists (fun (Flag flag, _mode) -> flag.name = domain.name)
- type dynamic = Dynamic: (unit -> 'v abstraction) with_info -> dynamic
-
let abstractions = ref []
- let dynamic_abstractions : dynamic list ref = ref []
+ let dynamic_abstractions = ref []
let register ~name ~descr ?(experimental=false) ?(priority=0) abstraction =
let descr = if experimental then "Experimental. " ^ descr else descr in
@@ -83,18 +81,16 @@ module Config = struct
abstractions := flag :: !abstractions;
flag
- let dynamic_register ~name ~descr ?(experimental=false) ?(priority=0) make =
- let descr = if experimental then "Experimental. " ^ descr else descr in
+ let dynamic_register ~name ~descr make =
Value_parameters.register_domain ~name ~descr;
- let dynamic = Dynamic { name; experimental; priority; abstraction=make; } in
- dynamic_abstractions := dynamic :: !dynamic_abstractions
+ dynamic_abstractions := (name, make) :: !dynamic_abstractions
let configure () =
let add_main_mode mode =
let main, _ = Globals.entry_point () in
(main, Domain_mode.Mode.all) :: mode
in
- let add config name make =
+ let add config (name, make) =
let enabled = Value_parameters.Domains.mem name in
try
let mode = Value_parameters.DomainsFunction.find name in
@@ -104,17 +100,10 @@ module Config = struct
if enabled then add (make (), None) config else config
in
let aux config (Flag domain as flag) =
- add config domain.name (fun () -> flag)
+ add config (domain.name, (fun () -> flag))
in
let config = List.fold_left aux empty !abstractions in
- let aux config (Dynamic { name; experimental; priority; abstraction; }) =
- let make () =
- let abstraction = abstraction () in
- Flag { name; experimental; priority; abstraction; }
- in
- add config name make
- in
- List.fold_left aux config !dynamic_abstractions
+ List.fold_left add config !dynamic_abstractions
(* --- Register default abstractions -------------------------------------- *)
diff --git a/src/plugins/value/engine/abstractions.mli b/src/plugins/value/engine/abstractions.mli
index 3f3ff8d674e..8c98ee9b149 100644
--- a/src/plugins/value/engine/abstractions.mli
+++ b/src/plugins/value/engine/abstractions.mli
@@ -94,8 +94,7 @@ 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 -> ?experimental:bool -> ?priority:int ->
- (unit -> 'v abstraction) -> unit
+ name:string -> descr:string -> (unit -> flag) -> unit
(** Reduced product between two value abstractions, identified by their keys. *)
type ('a, 'b) value_reduced_product =
--
GitLab