diff --git a/src/plugins/markdown-report/md_gen.ml b/src/plugins/markdown-report/md_gen.ml index 6e04b36275d3dee5747e3fac33396f868ba1ddd3..2c342d7285f90966395484b127e28bdba7f74925 100644 --- a/src/plugins/markdown-report/md_gen.ml +++ b/src/plugins/markdown-report/md_gen.ml @@ -39,28 +39,6 @@ let sanitize_anchor s = else if s.[0] = '_' then "a" ^ s else s -let all_eva_domains = - [ "-eva-apron-box", "box domain of the Apron library"; - "-eva-apron-oct", "octagon domain of the Apron library"; - "-eva-bitwise-domain", "domain for bitwise computations"; - "-eva-equality-domain", - "domain for storing equalities between memory locations"; - "-eva-gauges-domain", - "gauges domain for relations between memory locations and loop counter"; - "-eva-inout-domain", - "domain for input and output memory locations"; - "-eva-polka-equalities", - "linear equalities domain of the Apron library"; - "-eva-polka-loose", - "loose polyhedra domain of the Apron library"; - "-eva-polka-strict", - "strict polyhedra domain of the Apron library"; - "-eva-sign-domain", "sign domain (useful only for demos)"; - "-eva-symbolic-locations-domain", - "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 @@ -72,10 +50,10 @@ let plural l s = | _::_::_ -> s ^ "s" let get_eva_domains () = - Extlib.filter_map - (fun (x,_) -> Dynamic.Parameter.Bool.get x ()) - (fun (x,y) -> (plain "option" @ bold x), plain y) - all_eva_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 @@ -92,12 +70,12 @@ let section_domains env = | [] -> [Text (plain - "Only the base domain (`Cvalue`) \ + "Only the base domain (`cvalue`) \ has been used for the analysis")] | _ -> [Text (plain - "In addition to the base domain (`Cvalue`), additional \ + "In addition to the base domain (`cvalue`), additional \ domains have been used by EVA"); DL l] ) diff --git a/src/plugins/markdown-report/tests/eva/oracle/cwe126.0.md b/src/plugins/markdown-report/tests/eva/oracle/cwe126.0.md index b96d202aea52fd78e9f83eba955b70c5915354fa..27c8a338e969cbc8e5b7d9a85d04cbac815be920 100644 --- a/src/plugins/markdown-report/tests/eva/oracle/cwe126.0.md +++ b/src/plugins/markdown-report/tests/eva/oracle/cwe126.0.md @@ -28,7 +28,7 @@ that have been considered during the analysis are the following: ### EVA Domains {#domains} -Only the base domain (`Cvalue`) has been used for the analysis +Only the base domain (`cvalue`) has been used for the analysis ### Stubbed Functions {#stubs} 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 ../../.."