From db99b4b5105d79aac5c3b65e865e27fa8e91f981 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Wed, 18 Mar 2020 15:27:11 +0100
Subject: [PATCH] [Eva] Exports the list (name and description) of enabled
abstract domains.
Used by the markdown-report plugin.
---
src/plugins/markdown-report/md_gen.ml | 36 +++-----------------------
src/plugins/value/Eva.mli | 7 +++--
src/plugins/value/value_parameters.ml | 6 +++++
src/plugins/value/value_parameters.mli | 3 +++
4 files changed, 18 insertions(+), 34 deletions(-)
diff --git a/src/plugins/markdown-report/md_gen.ml b/src/plugins/markdown-report/md_gen.ml
index d3b3f7fa068..2c342d7285f 100644
--- a/src/plugins/markdown-report/md_gen.ml
+++ b/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
diff --git a/src/plugins/value/Eva.mli b/src/plugins/value/Eva.mli
index 14467f726e7..462e5bdab03 100644
--- a/src/plugins/value/Eva.mli
+++ b/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
diff --git a/src/plugins/value/value_parameters.ml b/src/plugins/value/value_parameters.ml
index 3f4f1fa94be..70311f618f1 100644
--- a/src/plugins/value/value_parameters.ml
+++ b/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"
diff --git a/src/plugins/value/value_parameters.mli b/src/plugins/value/value_parameters.mli
index bca2258cec9..8c338bbc48c 100644
--- a/src/plugins/value/value_parameters.mli
+++ b/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 ../../.."
--
GitLab