[Eva] New option -eva-domains that enables a list of domains.

src/plugins/value/engine/abstractions.ml

@@ -66,14 +66,17 @@ module Config = struct
   let dynamic_abstractions : dynamic list ref = ref []
 
   let register ~enable abstraction =
+    Value_parameters.register_domain abstraction.name;
     abstractions := (enable, Flag abstraction) :: !abstractions
 
   let dynamic_register ~configure ~make =
     dynamic_abstractions := Dynamic (configure, make) :: !dynamic_abstractions
 
   let configure () =
-    let aux config (enable, flag) =
-      if enable () then add flag config else config
+    let aux config (enable, (Flag domain as flag)) =
+      if enable () || Value_parameters.Domains.mem domain.name
+      then add flag config
+      else config
     in
     let config = List.fold_left aux empty !abstractions in
     let aux config (Dynamic (configure, make)) =

src/plugins/value/engine/abstractions.mli

@@ -68,8 +68,9 @@ type 'v abstraction =
     domain: 'v domain; (** The domain over the value abstraction. *)
   }
 
-(** Register an abstraction. The abstraction is used in an Eva analysis only if
-    [enable ()] returns true at the start of the analysis.  *)
+(** Register an abstraction. The abstraction is used in an Eva analysis if
+    [enable ()] returns true at the start of the analysis, or if -eva-domains
+    has been set to the name of the abstraction.  *)
 val register: enable:(unit -> bool) -> 'v abstraction -> unit
 
 (** Register a dynamic abstraction: the abstraction is built by applying

src/plugins/value/value_parameters.ml

@@ -124,8 +124,48 @@ let malloc = add_group "Dynamic allocation"
 (* --- Eva domains                                                        --- *)
 (* -------------------------------------------------------------------------- *)
 
+let () = Parameter_customize.set_group domains
+module Domains =
+  String_set
+    (struct
+      let option_name = "-eva-domains"
+      let arg_name = "d1,...,dn"
+      let help = "Enable a list of analysis domains."
+    end)
+let () = add_precision_dep Domains.parameter
+
+(* List of available domains. *)
+let domains_ref = ref []
+
+(* Help message for the -eva-domains option, with the list of currently
+   available domains. *)
+let domains_help () =
+  let pp_str_list = Pretty_utils.pp_list ~sep:", " Format.pp_print_string in
+  Format.asprintf
+    "Enable a list of analysis domains. Available domains are: %a"
+    pp_str_list (List.rev !domains_ref)
+
+(* Registers a new domain. Updates the help message of -eva-domains. *)
+let register_domain name =
+  Cmdline.replace_option_help
+    Domains.option_name "eva" domains (domains_help ());
+  domains_ref := name :: !domains_ref
+
+(* Checks that a domain has been registered. *)
+let check_domain domain =
+  if not (List.mem domain !domains_ref)
+  then
+    let pp_str_list = Pretty_utils.pp_list ~sep:",@ " Format.pp_print_string in
+    abort "invalid domain %S for option -eva-domains.@.Possible domains are: %a"
+      domain pp_str_list (List.rev !domains_ref)
+
+let () =
+  Domains.add_set_hook
+    (fun _old domains -> Datatype.String.Set.iter check_domain domains)
+
 (* Set of parameters defining the abstractions used in an Eva analysis. *)
-let parameters_abstractions = ref Typed_parameter.Set.empty
+let parameters_abstractions =
+  ref (Typed_parameter.Set.singleton Domains.parameter)
 
 (* This functor must be used to create parameters for new domains of Eva. *)
 module Domain_Parameter

src/plugins/value/value_parameters.mli

@@ -28,6 +28,8 @@ module EnumerateCond: Parameter_sig.Bool
 module OracleDepth: Parameter_sig.Int
 module ReductionDepth: Parameter_sig.Int
 
+module Domains: Parameter_sig.String_set
+
 module CvalueDomain: Parameter_sig.Bool
 module EqualityDomain: Parameter_sig.Bool
 module GaugesDomain: Parameter_sig.Bool
@@ -240,6 +242,8 @@ val dkey_callbacks : category
 (** Debug category used to print the usage of widenings. *)
 val dkey_widening : category
 
+(** Registers available domain names for the -eva-domains option. *)
+val register_domain: string -> unit
 
 (** Notifies that the binding to Apron domains is available. *)
 val register_apron: unit -> unit