diff --git a/src/plugins/value/domains/apron/apron_domain.ml b/src/plugins/value/domains/apron/apron_domain.ml
index f90feb0168a9b8a6d4090f1ae2d058095b95bc93..edd9d982bb73d0bef5cc60b3f8a3519ace398637 100644
--- a/src/plugins/value/domains/apron/apron_domain.ml
+++ b/src/plugins/value/domains/apron/apron_domain.ml
@@ -730,12 +730,11 @@ let make name (module Man: Input) =
let module Domain = Domain_builder.Complete (Make (Man)) in
let open Abstractions in
let descr =
- "Experimental binding to the " ^ name ^
- " domain of the Apron library. \
- See http://apron.cri.ensmp.fr/library for more details."
+ "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 { name; descr; priority = 1;
+ register { name; descr; experimental = true; priority = 1;
values = Single (module Main_values.Interval);
domain = Domain (module Domain); }
diff --git a/src/plugins/value/domains/numerors/numerors_domain.ml b/src/plugins/value/domains/numerors/numerors_domain.ml
index 7ee0698de11494b98c5f0eebd2c145fdbc972943..6db584569cb6adfcdf5a5c313cb284f7d4a33ad9 100644
--- a/src/plugins/value/domains/numerors/numerors_domain.ml
+++ b/src/plugins/value/domains/numerors/numerors_domain.ml
@@ -155,8 +155,9 @@ let () =
let open Abstractions in
let domain =
{ name = "numerors";
- descr = "Experimental. Infers ranges for the absolute and relative errors \
+ descr = "Infers ranges for the absolute and relative errors \
in floating-point computations. No support of loops.";
+ experimental = true;
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 1c54e5c95e4247aea998044655b012b2000a0c23..8fd8892b7086754c85879478573473007fdc9f5d 100644
--- a/src/plugins/value/engine/abstractions.ml
+++ b/src/plugins/value/engine/abstractions.ml
@@ -41,6 +41,7 @@ type 'v domain =
type 'v abstraction =
{ name: string;
descr: string;
+ experimental: bool;
priority: int;
values: 'v value;
domain: 'v domain; }
@@ -67,6 +68,11 @@ module Config = struct
let dynamic_abstractions : dynamic list ref = ref []
let register abstraction =
+ let abstraction =
+ if abstraction.experimental
+ then { abstraction with descr = "Experimental. " ^ abstraction.descr }
+ else abstraction
+ in
let { name; descr; } = abstraction in
Value_parameters.register_domain ~name ~descr;
abstractions := (Flag abstraction) :: !abstractions
@@ -91,13 +97,14 @@ module Config = struct
(* --- Register default abstractions -------------------------------------- *)
let create abstract = register abstract; Flag abstract
- let create_domain priority name descr values domain =
+ let create_domain ?(experimental=false) priority name descr values domain =
create
- { name; descr; priority; values = Single values; domain = Domain domain }
+ { name; descr; experimental; priority;
+ values = Single values; domain = Domain domain }
(* Register standard domains over cvalues. *)
- let make rank name descr =
- create_domain rank name descr (module Main_values.CVal)
+ let make ?experimental rank name descr =
+ create_domain ?experimental rank name descr (module Main_values.CVal)
let cvalue =
make 9 "cvalue"
@@ -115,6 +122,7 @@ module Config = struct
descr = "Infers equalities between syntactic C expressions. \
Makes the analysis less dependent on temporary variables and \
intermediate computations.";
+ experimental = false;
priority = 8;
values = Struct Abstract.Value.Unit;
domain = Functor (module Equality_domain.Make); }
@@ -142,13 +150,13 @@ module Config = struct
"Infers the sign of program variables."
(module Sign_value) (module Sign_domain)
- let inout = make 5 "inout"
- "Experimental. Infers the inputs and outputs of each function."
+ let inout = make 5 "inout" ~experimental:true
+ "Infers the inputs and outputs of each function."
(module Inout_domain.D)
let traces =
- make 2 "traces"
- "Experimental. Builds an over-approximation of all the traces that lead \
+ make 2 "traces" ~experimental:true
+ "Builds an over-approximation of all the traces that lead \
to a statement."
(module Traces_domain.D)
@@ -321,8 +329,16 @@ let add_domain (type v) (abstraction: v abstraction) (module Acc: Acc) =
module Dom = (val domain)
end : Acc)
+let warn_experimental abstraction =
+ if abstraction.experimental then
+ Value_parameters.(warning ~wkey:wkey_experimental
+ "The %s domain is experimental." abstraction.name)
+
let build_domain config abstract =
- let build (Config.Flag abstraction) acc = add_domain abstraction acc in
+ let build (Config.Flag abstraction) acc =
+ warn_experimental abstraction;
+ add_domain abstraction acc
+ in
(* Domains in the [config] are sorted by increasing priority: domains with
higher priority are added last: they will be at the top of the domains
tree, and thus will be processed first during the analysis. *)
diff --git a/src/plugins/value/engine/abstractions.mli b/src/plugins/value/engine/abstractions.mli
index d687e7481bd90d4e05099f191f2e1321ffaf6685..d27496d414d9daf322490f96c8311fdd32691e98 100644
--- a/src/plugins/value/engine/abstractions.mli
+++ b/src/plugins/value/engine/abstractions.mli
@@ -58,16 +58,18 @@ type 'v 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.
+ An abstraction marked as experimental emits a warning when enabled.
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. *)
+ { name: string; (** Name of the abstraction. Must be unique. *)
+ descr: string; (** Short description of the abstraction. *)
+ experimental: bool; (** Is the domain experimental? *)
+ priority: int; (** Domains with higher priority are processed first. *)
+ values: 'v value; (** The value abstraction. *)
+ domain: 'v domain ; (** The domain over the value abstraction. *)
}
(** Register an abstraction. The abstraction is used in an Eva analysis if
diff --git a/src/plugins/value/value_parameters.ml b/src/plugins/value/value_parameters.ml
index 92dd6f08791e7053ee211eda7a56359a6cf19700..3f4f1fa94be34e805413d153ba66878f86bdf1a4 100644
--- a/src/plugins/value/value_parameters.ml
+++ b/src/plugins/value/value_parameters.ml
@@ -77,8 +77,6 @@ let dkey_incompatible_states = register_category "incompatible-states"
let dkey_iterator = register_category "iterator"
let dkey_callbacks = register_category "callbacks"
let dkey_widening = register_category "widening"
-let dkey_experimental = register_category "experimental-ok"
-
let () =
let activate dkey = add_debug_keys dkey in
@@ -102,6 +100,7 @@ let () = set_warn_status wkey_missing_loop_unroll_for Log.Winactive
let wkey_signed_overflow = register_warn_category "signed-overflow"
let wkey_invalid_assigns = register_warn_category "invalid-assigns"
let () = set_warn_status wkey_invalid_assigns Log.Wfeedback
+let wkey_experimental = register_warn_category "experimental"
module ForceValues =
WithOutput
diff --git a/src/plugins/value/value_parameters.mli b/src/plugins/value/value_parameters.mli
index b9e5794d2d9830337417f0ccba77dd37c4c50f62..bca2258cec9aff02f34e07b6822e58a0fd109799 100644
--- a/src/plugins/value/value_parameters.mli
+++ b/src/plugins/value/value_parameters.mli
@@ -203,6 +203,9 @@ val wkey_signed_overflow : warn_category
(** Warning category for 'completely invalid' assigns clause *)
val wkey_invalid_assigns : warn_category
+(** Warning category for experimental domains or features. *)
+val wkey_experimental : warn_category
+
(** Debug category used to print information about invalid pointer comparisons*)
val dkey_pointer_comparison: category