Commit 62c282b6 authored by David Bühler's avatar David Bühler
Browse files

[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.
parent e1770d2b
...@@ -71,10 +71,8 @@ module Config = struct ...@@ -71,10 +71,8 @@ module Config = struct
let mem (Flag domain) = let mem (Flag domain) =
exists (fun (Flag flag, _mode) -> flag.name = domain.name) exists (fun (Flag flag, _mode) -> flag.name = domain.name)
type dynamic = Dynamic: (unit -> 'v abstraction) with_info -> dynamic
let abstractions = ref [] let abstractions = ref []
let dynamic_abstractions : dynamic list ref = ref [] let dynamic_abstractions = ref []
let register ~name ~descr ?(experimental=false) ?(priority=0) abstraction = let register ~name ~descr ?(experimental=false) ?(priority=0) abstraction =
let descr = if experimental then "Experimental. " ^ descr else descr in let descr = if experimental then "Experimental. " ^ descr else descr in
...@@ -83,18 +81,16 @@ module Config = struct ...@@ -83,18 +81,16 @@ module Config = struct
abstractions := flag :: !abstractions; abstractions := flag :: !abstractions;
flag flag
let dynamic_register ~name ~descr ?(experimental=false) ?(priority=0) make = let dynamic_register ~name ~descr make =
let descr = if experimental then "Experimental. " ^ descr else descr in
Value_parameters.register_domain ~name ~descr; Value_parameters.register_domain ~name ~descr;
let dynamic = Dynamic { name; experimental; priority; abstraction=make; } in dynamic_abstractions := (name, make) :: !dynamic_abstractions
dynamic_abstractions := dynamic :: !dynamic_abstractions
let configure () = let configure () =
let add_main_mode mode = let add_main_mode mode =
let main, _ = Globals.entry_point () in let main, _ = Globals.entry_point () in
(main, Domain_mode.Mode.all) :: mode (main, Domain_mode.Mode.all) :: mode
in in
let add config name make = let add config (name, make) =
let enabled = Value_parameters.Domains.mem name in let enabled = Value_parameters.Domains.mem name in
try try
let mode = Value_parameters.DomainsFunction.find name in let mode = Value_parameters.DomainsFunction.find name in
...@@ -104,17 +100,10 @@ module Config = struct ...@@ -104,17 +100,10 @@ module Config = struct
if enabled then add (make (), None) config else config if enabled then add (make (), None) config else config
in in
let aux config (Flag domain as flag) = let aux config (Flag domain as flag) =
add config domain.name (fun () -> flag) add config (domain.name, (fun () -> flag))
in in
let config = List.fold_left aux empty !abstractions in let config = List.fold_left aux empty !abstractions in
let aux config (Dynamic { name; experimental; priority; abstraction; }) = List.fold_left add config !dynamic_abstractions
let make () =
let abstraction = abstraction () in
Flag { name; experimental; priority; abstraction; }
in
add config name make
in
List.fold_left aux config !dynamic_abstractions
(* --- Register default abstractions -------------------------------------- *) (* --- Register default abstractions -------------------------------------- *)
......
...@@ -94,8 +94,7 @@ val register: ...@@ -94,8 +94,7 @@ val register:
the last argument when starting an analysis, if the -eva-domains option the last argument when starting an analysis, if the -eva-domains option
has been set to [name]. See function {!register} for more details. *) has been set to [name]. See function {!register} for more details. *)
val dynamic_register: val dynamic_register:
name:string -> descr:string -> ?experimental:bool -> ?priority:int -> name:string -> descr:string -> (unit -> flag) -> unit
(unit -> 'v abstraction) -> unit
(** Reduced product between two value abstractions, identified by their keys. *) (** Reduced product between two value abstractions, identified by their keys. *)
type ('a, 'b) value_reduced_product = type ('a, 'b) value_reduced_product =
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment