diff --git a/src/plugins/value/engine/abstractions.ml b/src/plugins/value/engine/abstractions.ml index ac5b7613dc70578f63cf3864a11ddf52de36e80a..daa7f30ed177b799041c8f00eb03aca7927a6fa5 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 f5592ba0d4776acb070cac23261764f1b0545a40..86d09020a75375033a7ef211124a8143067d39d7 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 =