diff --git a/src/plugins/markdown-report/md_gen.ml b/src/plugins/markdown-report/md_gen.ml index d3b3f7fa0686c583e9a2616e53a162ce999e2402..2c342d7285f90966395484b127e28bdba7f74925 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 14467f726e7d8e55b56e6f96ab30453175375675..462e5bdab037f40b4661b084d4ba81580f22bdc2 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 3f4f1fa94be34e805413d153ba66878f86bdf1a4..70311f618f178f9f657a7a05ea338807f30a14d1 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 bca2258cec9aff02f34e07b6822e58a0fd109799..8c338bbc48c349b742d7af40e1ae39b0e4a580b8 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 ../../.."