Merge branch 'fix/markdown-report/eva-domains' into 'master'

[mdr] Uses the -eva-domains option instead of multiple options -eva-*-domain.

See merge request frama-c/frama-c!2579

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]
       )

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}

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 ../../.."