diff --git a/src/plugins/value/domains/apron/apron_domain.ml b/src/plugins/value/domains/apron/apron_domain.ml
index 4d8ee2d686dea1f01f64d755439d64f7dadafd48..d978ca8f1360b3b3c3496d112475df6b0a32da98 100644
--- a/src/plugins/value/domains/apron/apron_domain.ml
+++ b/src/plugins/value/domains/apron/apron_domain.ml
@@ -729,17 +729,23 @@ let () = Floating_point.set_round_nearest_even ()
let make name enable (module Man: Input) =
let module Domain = Domain_builder.Complete (Make (Man)) in
let open Abstractions in
- register ~enable { name; priority = 1;
+ let descr =
+ "Experimental binding to the " ^ name ^
+ " domain of the Apron library. \
+ See http://apron.cri.ensmp.fr/library for more details."
+ in
+ let name = "apron-" ^ name in
+ register ~enable { name; descr; priority = 1;
values = Single (module Main_values.Interval);
domain = Domain (module Domain); }
let () =
let open Value_parameters in
- make "apron-octagon" ApronOctagon.get (module Apron_Octagon);
- make "apron-box" ApronBox.get (module Apron_Box);
- make "apron-polka-loose" PolkaLoose.get (module Apron_Polka_Loose);
- make "apron-polka-strict" PolkaStrict.get (module Apron_Polka_Strict);
- make "apron-polka-equality" PolkaEqualities.get (module Apron_Polka_Equalities);
+ make "octagon" ApronOctagon.get (module Apron_Octagon);
+ make "box" ApronBox.get (module Apron_Box);
+ make "polka-loose" PolkaLoose.get (module Apron_Polka_Loose);
+ make "polka-strict" PolkaStrict.get (module Apron_Polka_Strict);
+ make "polka-equality" PolkaEqualities.get (module Apron_Polka_Equalities);
register_apron ()
diff --git a/src/plugins/value/domains/numerors/numerors_domain.ml b/src/plugins/value/domains/numerors/numerors_domain.ml
index 9d54d1548b56778c7c8c062d8ad772f1addafd0a..b7d3142cede4d5a7c03cbdbc7f238da811ffb759 100644
--- a/src/plugins/value/domains/numerors/numerors_domain.ml
+++ b/src/plugins/value/domains/numerors/numerors_domain.ml
@@ -155,6 +155,8 @@ let () =
let open Abstractions in
let domain =
{ name = "numerors";
+ descr = "Experimental. Infers ranges for the absolute and relative errors \
+ in floating-point computations. No support of loops.";
priority = 0;
values = Single (module Numerors_value);
domain = Domain (module Domain); }
diff --git a/src/plugins/value/engine/abstractions.ml b/src/plugins/value/engine/abstractions.ml
index 82365793479ab3a3fd25632cb2eeb8628fd71763..f679e5d78154b012ccde9377ad258cd097805f62 100644
--- a/src/plugins/value/engine/abstractions.ml
+++ b/src/plugins/value/engine/abstractions.ml
@@ -40,6 +40,7 @@ type 'v domain =
type 'v abstraction =
{ name: string;
+ descr: string;
priority: int;
values: 'v value;
domain: 'v domain; }
@@ -66,7 +67,8 @@ module Config = struct
let dynamic_abstractions : dynamic list ref = ref []
let register ~enable abstraction =
- Value_parameters.register_domain abstraction.name;
+ let { name; descr; } = abstraction in
+ Value_parameters.register_domain ~name ~descr;
abstractions := (enable, Flag abstraction) :: !abstractions
let dynamic_register ~configure ~make =
@@ -89,42 +91,74 @@ module Config = struct
(* --- Register default abstractions -------------------------------------- *)
let create ~enable abstract = register ~enable abstract; Flag abstract
- let create_domain priority name enable values domain =
+ let create_domain priority name descr enable values domain =
create ~enable
- { name; priority; values = Single values; domain = Domain domain }
+ { name; descr; priority; values = Single values; domain = Domain domain }
open Value_parameters
(* Register standard domains over cvalues. *)
- let make rank name enable =
- create_domain rank name enable (module Main_values.CVal)
+ let make rank name descr enable =
+ create_domain rank name descr enable (module Main_values.CVal)
- let cvalue = make 9 "cvalue" CvalueDomain.get (module Cvalue_domain.State)
+ let cvalue =
+ make 9 "cvalue"
+ "Main analysis domain, enabled by default. Should not be disabled."
+ CvalueDomain.get (module Cvalue_domain.State)
let symbolic_locations =
- make 7 "symbolic-locations" SymbolicLocsDomain.get (module Symbolic_locs.D)
+ make 7 "symbolic-locations"
+ "Infers values of symbolic locations represented by imprecise lvalues, \
+ such as t[i] or *p when the possible values of [i] or [p] are imprecise."
+ SymbolicLocsDomain.get (module Symbolic_locs.D)
let equality_domain =
{ name = "equality";
+ descr = "Infers equalities between syntactic C expressions. \
+ Makes the analysis less dependent on temporary variables and \
+ intermediate computations.";
priority = 8;
values = Struct Abstract.Value.Unit;
domain = Functor (module Equality_domain.Make); }
let equality = create ~enable:EqualityDomain.get equality_domain
- let gauges = make 6 "gauges" GaugesDomain.get (module Gauges_domain.D)
- let octagon = make 6 "octagon" OctagonDomain.get (module Octagons)
+ let gauges =
+ make 6 "gauges"
+ "Infers linear inequalities between the variables modified within a loop \
+ and a special loop counter."
+ GaugesDomain.get (module Gauges_domain.D)
+
+ let octagon =
+ make 6 "octagon"
+ "Infers relations between scalar variables of the form b ≤ ±X ± Y ≤ e, \
+ where X, Y are program variables and b, e are constants."
+ OctagonDomain.get (module Octagons)
let bitwise =
- create_domain 3 "bitwise" BitwiseOffsmDomain.get
- (module Offsm_value.Offsm) (module Offsm_domain.D)
+ create_domain 3 "bitwise"
+ "Infers bitwise information to interpret more precisely bitwise operators."
+ BitwiseOffsmDomain.get (module Offsm_value.Offsm) (module Offsm_domain.D)
let sign =
- create_domain 4 "sign" SignDomain.get
- (module Sign_value) (module Sign_domain)
-
- let inout = make 5 "inout" InoutDomain.get (module Inout_domain.D)
- let traces = make 2 "traces" TracesDomain.get (module Traces_domain.D)
- let printer = make 2 "printer" PrinterDomain.get (module Printer_domain)
+ create_domain 4 "sign"
+ "Infers the sign of program variables."
+ SignDomain.get (module Sign_value) (module Sign_domain)
+
+ let inout = make 5 "inout"
+ "Experimental. Infers the inputs and outputs of each function."
+ InoutDomain.get (module Inout_domain.D)
+
+ let traces =
+ make 2 "traces"
+ "Experimental. Builds an over-approximation of all the traces that lead \
+ to a statement."
+ TracesDomain.get (module Traces_domain.D)
+
+ let printer =
+ make 2 "printer"
+ "Debug domain, only useful for developers. Prints the transfer functions \
+ used during the analysis."
+ PrinterDomain.get (module Printer_domain)
(* --- Default and legacy configurations ---------------------------------- *)
diff --git a/src/plugins/value/engine/abstractions.mli b/src/plugins/value/engine/abstractions.mli
index ab22ede69a23fe3f154c6bb91824d68b944912bf..9ccac22fb48203b2bcf5ce06292a52c55da862b6 100644
--- a/src/plugins/value/engine/abstractions.mli
+++ b/src/plugins/value/engine/abstractions.mli
@@ -57,12 +57,14 @@ type 'v domain =
| Functor: (module domain_functor) -> _ domain
(** Abstraction to be registered. The name of each abstraction must be unique.
+ The description is printed in the help message of the -eva-domains option.
The priority can be any integer; domains with higher priority are always
processed first. The domains currently provided by Eva have priority ranging
between 1 and 19, so a priority of 0 (respectively 20) ensures that a new
domain is processed after (respectively before) the classic Eva domains. *)
type 'v abstraction =
{ name: string; (** Name of the abstraction. Must be unique. *)
+ descr: string; (** Short description of the abstraction. *)
priority: int; (** Domains with higher priority are processed first. *)
values: 'v value; (** The value abstraction. *)
domain: 'v domain; (** The domain over the value abstraction. *)
diff --git a/src/plugins/value/value_parameters.ml b/src/plugins/value/value_parameters.ml
index b916fb9346bde72df2f4a3260db60788d4379736..4ee2d35357174a64eabd0596aa4e4329a16ea136 100644
--- a/src/plugins/value/value_parameters.ml
+++ b/src/plugins/value/value_parameters.ml
@@ -134,7 +134,7 @@ module Domains =
end)
let () = add_precision_dep Domains.parameter
-(* List of available domains. *)
+(* List (name, descr) of available domains. *)
let domains_ref = ref []
(* Help message for the -eva-domains option, with the list of currently
@@ -142,22 +142,36 @@ let domains_ref = ref []
let domains_help () =
let pp_str_list = Pretty_utils.pp_list ~sep:", " Format.pp_print_string in
Format.asprintf
- "Enable a list of analysis domains. Available domains are: %a"
- pp_str_list (List.rev !domains_ref)
+ "Enable a list of analysis domains. Available domains are: %a. \
+ Use -eva-domains help to print a short description of each domain."
+ pp_str_list (List.rev_map fst !domains_ref)
+
+(* Prints the list of available domains with their description. *)
+let domains_list () =
+ let pp_dom fmt (name, descr) =
+ Format.fprintf fmt "%-20s @[%t@]" name
+ (fun fmt -> Format.pp_print_text fmt descr)
+ in
+ feedback ~level:0
+ "List of available domains:@. %a@."
+ (Pretty_utils.pp_list ~sep:"@," pp_dom) (List.rev !domains_ref);
+ raise Cmdline.Exit
(* Registers a new domain. Updates the help message of -eva-domains. *)
-let register_domain name =
+let register_domain ~name ~descr =
+ domains_ref := (name, descr) :: !domains_ref;
Cmdline.replace_option_help
- Domains.option_name "eva" domains (domains_help ());
- domains_ref := name :: !domains_ref
+ Domains.option_name "eva" domains (domains_help ())
(* Checks that a domain has been registered. *)
let check_domain domain =
- if not (List.mem domain !domains_ref)
+ if domain = "help" || domain = "list"
+ then domains_list ()
+ else if not (List.exists (fun (name, _) -> name = domain) !domains_ref)
then
let pp_str_list = Pretty_utils.pp_list ~sep:",@ " Format.pp_print_string in
abort "invalid domain %S for option -eva-domains.@.Possible domains are: %a"
- domain pp_str_list (List.rev !domains_ref)
+ domain pp_str_list (List.rev_map fst !domains_ref)
let () =
Domains.add_set_hook
diff --git a/src/plugins/value/value_parameters.mli b/src/plugins/value/value_parameters.mli
index 8c89a2525809b8c38a4c43c234466c0d8861745d..5f69dfefce3ef5a4e8914b1bcc93e2a983be8444 100644
--- a/src/plugins/value/value_parameters.mli
+++ b/src/plugins/value/value_parameters.mli
@@ -243,7 +243,7 @@ val dkey_callbacks : category
val dkey_widening : category
(** Registers available domain names for the -eva-domains option. *)
-val register_domain: string -> unit
+val register_domain: name:string -> descr:string -> unit
(** Notifies that the binding to Apron domains is available. *)
val register_apron: unit -> unit