Merge branch 'feature/eva/dynamic-register' into 'master'

[Eva] Simplify the usage of Abstraction.dynamic_register

See merge request frama-c/frama-c!3473

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 =

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 =