[Eva] Exports the list (name and description) of enabled abstract domains.

Used by the markdown-report plugin.

src/plugins/markdown-report/md_gen.ml

@@ -39,27 +39,6 @@ let sanitize_anchor s =
   else if s.[0] = '_' then "a" ^ s
   else s
 
-let all_eva_domains =
-  [ "apron-box", "box domain of the Apron library";
-    "apron-oct", "octagon domain of the Apron library";
-    "apron-polka-equalities", "linear equalities domain of the Apron library";
-    "apron-polka-loose", "loose polyhedra domain of the Apron library";
-    "apron-polka-strict", "strict polyhedra domain of the Apron library";
-    "bitwise", "domain for bitwise computations";
-    "equality", "domain for storing equalities between memory locations";
-    "gauges", "gauges domain for relations between memory locations \
-               and loop counter";
-    "inout", "domain for input and output memory locations";
-    "octagon", "domain inferring relations b ≤ ±X ± Y ≤ e between pairs of \
-                integer variables X and Y.";
-    "numerors", "domain computing absolute and relative errors \
-                 of floating-point computations";
-    "sign", "sign domain (useful only for demos)";
-    "symbolic-locations",
-    "domain computing ranges of variation for symbolic locations \
-     (e.g. `a[i]` when `i` is not precisely known by `Cvalue`)"
-  ]
-
 let insert_marks env anchor =
   Comment "BEGIN_REMARK"
   :: insert_remark env anchor
@@ -71,17 +50,10 @@ let plural l s =
   | _::_::_ -> s ^ "s"
 
 let get_eva_domains () =
-  let eva_domains = Dynamic.Parameter.String.get "-eva-domains" () in
-  let domains_list = String.split_on_char ',' eva_domains in
-  let alternative_domains = List.filter ((<>) "cvalue") domains_list in
-  let aux domain =
-    let descr =
-      try List.assoc domain all_eva_domains
-      with Not_found -> ""
-    in
-    (plain "domain" @ bold domain), plain descr
-  in
-  List.map aux alternative_domains
+  let eva_domains = Eva.Value_parameters.enabled_domains () in
+  let domains = List.filter (fun (name, _) -> name <> "cvalue") eva_domains in
+  let aux (name, descr) = (plain "domain" @ bold name), plain descr in
+  List.map aux domains
 
 let section_domains env =
   let anchor = "domains" in

src/plugins/value/Eva.mli

@@ -22,8 +22,6 @@
 
 (** Analysis for values and pointers *)
 
-(** No function is directly exported: they are registered in {!Db.Value}. *)
-
 module Value_results: sig
   type results
 
@@ -33,3 +31,8 @@ module Value_results: sig
   val change_callstacks:
     (Value_types.callstack -> Value_types.callstack) -> results -> results
 end
+
+module Value_parameters: sig
+  (** Returns the list (name, descr) of currently enabled abstract domains. *)
+  val enabled_domains: unit -> (string * string) list
+end

src/plugins/value/value_parameters.ml

@@ -193,6 +193,12 @@ let register_domain ~name ~descr =
   Cmdline.replace_option_help
     Domains.option_name "eva" domains (domains_help ())
 
+let enabled_domains () =
+  let domains = Domains.get () in
+  List.filter
+    (fun (name, _) -> Datatype.String.Set.mem name domains)
+    !domains_ref
+
 (* Checks that a domain has been registered. *)
 let check_domain domain =
   if domain = "help" || domain = "list"

src/plugins/value/value_parameters.mli

@@ -230,6 +230,9 @@ val dkey_widening : category
 (** Registers available domain names for the -eva-domains option. *)
 val register_domain: name:string -> descr:string -> unit
 
+(** Returns the list (name, descr) of currently enabled domains. *)
+val enabled_domains: unit -> (string * string) list
+
 (*
 Local Variables:
 compile-command: "make -C ../../.."