diff --git a/src/plugins/value/domains/apron/apron_domain.ml b/src/plugins/value/domains/apron/apron_domain.ml
index d978ca8f1360b3b3c3496d112475df6b0a32da98..f90feb0168a9b8a6d4090f1ae2d058095b95bc93 100644
--- a/src/plugins/value/domains/apron/apron_domain.ml
+++ b/src/plugins/value/domains/apron/apron_domain.ml
@@ -726,7 +726,7 @@ end
(** Apron manager allocation changes the rounding mode. *)
let () = Floating_point.set_round_nearest_even ()
-let make name enable (module Man: Input) =
+let make name (module Man: Input) =
let module Domain = Domain_builder.Complete (Make (Man)) in
let open Abstractions in
let descr =
@@ -735,18 +735,16 @@ let make name enable (module Man: Input) =
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); }
+ register { name; descr; priority = 1;
+ values = Single (module Main_values.Interval);
+ domain = Domain (module Domain); }
let () =
- let open Value_parameters in
- 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 ()
+ make "octagon" (module Apron_Octagon);
+ make "box" (module Apron_Box);
+ make "polka-loose" (module Apron_Polka_Loose);
+ make "polka-strict" (module Apron_Polka_Strict);
+ make "polka-equality" (module Apron_Polka_Equalities);
(*
diff --git a/src/plugins/value/domains/numerors/numerors_domain.ml b/src/plugins/value/domains/numerors/numerors_domain.ml
index b7d3142cede4d5a7c03cbdbc7f238da811ffb759..7ee0698de11494b98c5f0eebd2c145fdbc972943 100644
--- a/src/plugins/value/domains/numerors/numerors_domain.ml
+++ b/src/plugins/value/domains/numerors/numerors_domain.ml
@@ -162,7 +162,6 @@ let () =
domain = Domain (module Domain); }
in
let reduced_product = Main_values.CVal.key, Numerors_value.key, reduce_error in
- register ~enable:Value_parameters.NumerorsDomain.get domain;
+ register domain;
register_value_reduction reduced_product;
- register_hook reduce_cast;
- Value_parameters.register_numerors ()
+ register_hook reduce_cast
diff --git a/src/plugins/value/domains/numerors/numerors_domain.mli b/src/plugins/value/domains/numerors/numerors_domain.mli
index abc7c6322c4e4dfe6f9ae6ba51d6637307e0618f..7d1a78bc4f0d0ae2f6e65660566e2a5773749cf5 100644
--- a/src/plugins/value/domains/numerors/numerors_domain.mli
+++ b/src/plugins/value/domains/numerors/numerors_domain.mli
@@ -23,4 +23,4 @@
(** Numerors domain: computes over-approximations of the rounding errors bounds
of floating-point computations.
Nothing is exported: the domain is registered as an analysis abstraction
- in the Eva engine, enabled by the -eva-numerors-domain option. *)
+ in the Eva engine, enabled by the -eva-domains numerors option. *)
diff --git a/src/plugins/value/engine/abstractions.ml b/src/plugins/value/engine/abstractions.ml
index f679e5d78154b012ccde9377ad258cd097805f62..1c54e5c95e4247aea998044655b012b2000a0c23 100644
--- a/src/plugins/value/engine/abstractions.ml
+++ b/src/plugins/value/engine/abstractions.ml
@@ -66,17 +66,17 @@ module Config = struct
let abstractions = ref []
let dynamic_abstractions : dynamic list ref = ref []
- let register ~enable abstraction =
+ let register abstraction =
let { name; descr; } = abstraction in
Value_parameters.register_domain ~name ~descr;
- abstractions := (enable, Flag abstraction) :: !abstractions
+ abstractions := (Flag abstraction) :: !abstractions
let dynamic_register ~configure ~make =
dynamic_abstractions := Dynamic (configure, make) :: !dynamic_abstractions
let configure () =
- let aux config (enable, (Flag domain as flag)) =
- if enable () || Value_parameters.Domains.mem domain.name
+ let aux config (Flag domain as flag) =
+ if Value_parameters.Domains.mem domain.name
then add flag config
else config
in
@@ -90,27 +90,25 @@ module Config = struct
(* --- Register default abstractions -------------------------------------- *)
- let create ~enable abstract = register ~enable abstract; Flag abstract
- let create_domain priority name descr enable values domain =
- create ~enable
+ let create abstract = register abstract; Flag abstract
+ let create_domain priority name descr values domain =
+ create
{ name; descr; priority; values = Single values; domain = Domain domain }
- open Value_parameters
-
(* Register standard domains over cvalues. *)
- let make rank name descr enable =
- create_domain rank name descr enable (module Main_values.CVal)
+ let make rank name descr =
+ create_domain rank name descr (module Main_values.CVal)
let cvalue =
make 9 "cvalue"
"Main analysis domain, enabled by default. Should not be disabled."
- CvalueDomain.get (module Cvalue_domain.State)
+ (module Cvalue_domain.State)
let symbolic_locations =
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)
+ (module Symbolic_locs.D)
let equality_domain =
{ name = "equality";
@@ -120,45 +118,45 @@ module Config = struct
priority = 8;
values = Struct Abstract.Value.Unit;
domain = Functor (module Equality_domain.Make); }
- let equality = create ~enable:EqualityDomain.get equality_domain
+ let equality = create equality_domain
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)
+ (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)
+ (module Octagons)
let bitwise =
create_domain 3 "bitwise"
"Infers bitwise information to interpret more precisely bitwise operators."
- BitwiseOffsmDomain.get (module Offsm_value.Offsm) (module Offsm_domain.D)
+ (module Offsm_value.Offsm) (module Offsm_domain.D)
let sign =
create_domain 4 "sign"
"Infers the sign of program variables."
- SignDomain.get (module Sign_value) (module Sign_domain)
+ (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)
+ (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)
+ (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)
+ (module Printer_domain)
(* --- Default and legacy configurations ---------------------------------- *)
diff --git a/src/plugins/value/engine/abstractions.mli b/src/plugins/value/engine/abstractions.mli
index 9ccac22fb48203b2bcf5ce06292a52c55da862b6..d687e7481bd90d4e05099f191f2e1321ffaf6685 100644
--- a/src/plugins/value/engine/abstractions.mli
+++ b/src/plugins/value/engine/abstractions.mli
@@ -71,9 +71,8 @@ type 'v abstraction =
}
(** Register an abstraction. The abstraction is used in an Eva analysis if
- [enable ()] returns true at the start of the analysis, or if -eva-domains
- has been set to the name of the abstraction. *)
-val register: enable:(unit -> bool) -> 'v abstraction -> unit
+ -eva-domains has been set to the name of the abstraction. *)
+val register: 'v abstraction -> unit
(** Register a dynamic abstraction: the abstraction is built by applying
[make (configure ())] at the start of each analysis. *)
diff --git a/src/plugins/value/value_parameters.ml b/src/plugins/value/value_parameters.ml
index 4ee2d35357174a64eabd0596aa4e4329a16ea136..92dd6f08791e7053ee211eda7a56359a6cf19700 100644
--- a/src/plugins/value/value_parameters.ml
+++ b/src/plugins/value/value_parameters.ml
@@ -126,14 +126,44 @@ let malloc = add_group "Dynamic allocation"
let () = Parameter_customize.set_group domains
module Domains =
- String_set
+ Filled_string_set
(struct
let option_name = "-eva-domains"
let arg_name = "d1,...,dn"
let help = "Enable a list of analysis domains."
+ let default = Datatype.String.Set.singleton "cvalue"
end)
let () = add_precision_dep Domains.parameter
+let remove_domain name =
+ Domains.set (Datatype.String.Set.filter ((!=) name) (Domains.get ()))
+
+(* For backward compatibility, creates an invisible option for the domain [name]
+ that sets up -eva-domains with [name]. To be removed one day. *)
+let create_domain_option name =
+ let option_name =
+ match name with
+ | "apron-box" -> "-eva-apron-box"
+ | "apron-octagon" -> "-eva-apron-oct"
+ | "apron-polka-loose" -> "-eva-polka-loose"
+ | "apron-polka-strict" -> "-eva-polka-strict"
+ | "apron-polka-equality" -> "-eva-polka-equalities"
+ | _ -> "-eva-" ^ name ^ "-domain"
+ in
+ let module Input = struct
+ let option_name = option_name
+ let help = "Use the " ^ name ^ " domain of eva."
+ let default = name = "cvalue"
+ end in
+ Parameter_customize.set_group domains;
+ Parameter_customize.is_invisible ();
+ let module Parameter = Bool (Input) in
+ Parameter.add_set_hook
+ (fun _old _new ->
+ warning "Option %s is deprecated. Use -eva-domains %s%s instead."
+ option_name (if _new then "" else "-") name;
+ if _new then Domains.add name else remove_domain name)
+
(* List (name, descr) of available domains. *)
let domains_ref = ref []
@@ -159,6 +189,7 @@ let domains_list () =
(* Registers a new domain. Updates the help message of -eva-domains. *)
let register_domain ~name ~descr =
+ create_domain_option name;
domains_ref := (name, descr) :: !domains_ref;
Cmdline.replace_option_help
Domains.option_name "eva" domains (domains_help ())
@@ -181,164 +212,6 @@ let () =
let parameters_abstractions =
ref (Typed_parameter.Set.singleton Domains.parameter)
-(* This functor must be used to create parameters for new domains of Eva. *)
-module Domain_Parameter
- (X:sig include Parameter_sig.Input val default: bool end)
-= struct
- Parameter_customize.set_group domains;
- module Parameter = Bool (X);;
- add_precision_dep Parameter.parameter;
- parameters_abstractions :=
- Typed_parameter.Set.add Parameter.parameter !parameters_abstractions;
- include Parameter
-end
-
-module CvalueDomain = Domain_Parameter
- (struct
- let option_name = "-eva-cvalue-domain"
- let help = "Use the default domain of eva."
- let default = true
- end)
-
-module EqualityDomain = Domain_Parameter
- (struct
- let option_name = "-eva-equality-domain"
- let help = "Use the equality domain of Eva."
- let default = false
- end)
-
-module GaugesDomain = Domain_Parameter
- (struct
- let option_name = "-eva-gauges-domain"
- let help = "Use the gauges domain of Eva."
- let default = false
- end)
-
-module SymbolicLocsDomain = Domain_Parameter
- (struct
- let option_name = "-eva-symbolic-locations-domain"
- let help = "Use a dedicated domain for symbolic equalities."
- let default = false
- end)
-
-module OctagonDomain = Domain_Parameter
- (struct
- let option_name = "-eva-octagon-domain"
- let help = "Use the octagon domain of Eva."
- let default = false
- end)
-
-module BitwiseOffsmDomain = Domain_Parameter
- (struct
- let option_name = "-eva-bitwise-domain"
- let help = "Use the bitwise abstractions of Eva."
- let default = false
- end)
-
-let numerors_available = ref false
-let register_numerors () = numerors_available := true
-
-let numerors_hook _ _ =
- if not !numerors_available
- then
- abort
- "The numerors domain has been requested but is not available,@ \
- as Frama-C did not found the MPFR library. The analysis is aborted."
- else if not (is_debug_key_enabled dkey_experimental) then
- warning "The numerors domain is experimental.";
-
-module NumerorsDomain = Domain_Parameter
- (struct
- let option_name = "-eva-numerors-domain"
- let help = "Experimental. Use the numerors domain of Eva. This domain \
- computes rounding error bounds for the floating point \
- computations"
- let default = false
- end)
-let () = NumerorsDomain.add_set_hook numerors_hook
-
-let apron_help = "Experimental binding of the numerical domains provided \
- by the APRON library: http://apron.cri.ensmp.fr/library \n"
-
-let apron_available = ref false
-let register_apron () = apron_available := true
-
-let apron_hook _ _ =
- if not !apron_available
- then
- abort "an Apron domain is requested but the apron binding is not available."
- else if not (is_debug_key_enabled dkey_experimental) then
- warning "The Apron domains binding is experimental.";
-
-module ApronOctagon = Domain_Parameter
- (struct
- let option_name = "-eva-apron-oct"
- let help = apron_help ^ "Use the octagon domain of apron."
- let default = false
- end)
-let () = ApronOctagon.add_set_hook apron_hook
-
-module ApronBox = Domain_Parameter
- (struct
- let option_name = "-eva-apron-box"
- let help = apron_help ^ "Use the box domain of apron."
- let default = false
- end)
-let () = ApronBox.add_set_hook apron_hook
-
-module PolkaLoose = Domain_Parameter
- (struct
- let option_name = "-eva-polka-loose"
- let help = apron_help ^ "Use the loose polyhedra domain of apron."
- let default = false
- end)
-let () = PolkaLoose.add_set_hook apron_hook
-
-module PolkaStrict = Domain_Parameter
- (struct
- let option_name = "-eva-polka-strict"
- let help = apron_help ^ "Use the strict polyhedra domain of apron."
- let default = false
- end)
-let () = PolkaStrict.add_set_hook apron_hook
-
-module PolkaEqualities = Domain_Parameter
- (struct
- let option_name = "-eva-polka-equalities"
- let help = apron_help ^ "Use the linear equalities domain of apron."
- let default = false
- end)
-let () = PolkaEqualities.add_set_hook apron_hook
-
-module InoutDomain = Domain_Parameter
- (struct
- let option_name = "-eva-inout-domain"
- let help = "Compute inputs and outputs within Eva. Experimental."
- let default = false
- end)
-
-module SignDomain = Domain_Parameter
- (struct
- let option_name = "-eva-sign-domain"
- let help = "Use the sign domain of Eva. For demonstration purposes only."
- let default = false
- end)
-
-module TracesDomain = Domain_Parameter
- (struct
- let option_name = "-eva-traces-domain"
- let help = "Use a domain to record traces of Eva. Experimental."
- let default = false
- end)
-
-module PrinterDomain = Domain_Parameter
- (struct
- let option_name = "-eva-printer-domain"
- let help = "Use the printer domain of eva. Useful for the developpers \
- of new abstract domains, as it prints the domain functions \
- that are called by Eva during an analysis."
- let default = false
- end)
let () = Parameter_customize.set_group domains
module EqualityCall =
@@ -1599,6 +1472,14 @@ let bind (type t) (module P: Parameter_sig.S with type t = t) f =
let set = set (module P) in
configures := (fun n -> set ~default:(n < 0) (f n)) :: !configures
+let domains n =
+ let (<+>) domains (x, name) = if n >= x then name :: domains else domains in
+ [ "cvalue" ]
+ <+> (1, "symbolic-locations")
+ <+> (2, "equality")
+ <+> (3, "gauges")
+ <+> (5, "octagon")
+
(* power 0 1 2 3 4 5 6 7 8 9 10 11 *)
let slevel_power = [| 0; 10; 20; 35; 60; 100; 160; 250; 500; 1000; 2000; 5000 |]
let ilevel_power = [| 8; 12; 16; 24; 32; 48; 64; 128; 192; 256; 256; 256 |]
@@ -1617,11 +1498,8 @@ let () =
bind (module ArrayPrecisionLevel) (get plevel_power);
bind (module LinearLevel) (fun n -> n * 20);
bind (module RmAssert) (fun n -> n > 0);
- bind (module SymbolicLocsDomain) (fun n -> n > 0);
- bind (module EqualityDomain) (fun n -> n > 1);
- bind (module GaugesDomain) (fun n -> n > 2);
+ bind (module Domains) (fun n -> Datatype.String.Set.of_list (domains n));
bind (module SplitReturn) (fun n -> if n > 3 then "auto" else "");
- bind (module OctagonDomain) (fun n -> n > 4);
bind (module EqualityCall) (fun n -> if n > 4 then "formals" else "none");
bind (module OctagonCall) (fun n -> n > 6);
()
diff --git a/src/plugins/value/value_parameters.mli b/src/plugins/value/value_parameters.mli
index 5f69dfefce3ef5a4e8914b1bcc93e2a983be8444..b9e5794d2d9830337417f0ccba77dd37c4c50f62 100644
--- a/src/plugins/value/value_parameters.mli
+++ b/src/plugins/value/value_parameters.mli
@@ -30,24 +30,6 @@ module ReductionDepth: Parameter_sig.Int
module Domains: Parameter_sig.String_set
-module CvalueDomain: Parameter_sig.Bool
-module EqualityDomain: Parameter_sig.Bool
-module GaugesDomain: Parameter_sig.Bool
-module SymbolicLocsDomain: Parameter_sig.Bool
-module OctagonDomain: Parameter_sig.Bool
-module BitwiseOffsmDomain: Parameter_sig.Bool
-module InoutDomain: Parameter_sig.Bool
-module SignDomain: Parameter_sig.Bool
-module PrinterDomain: Parameter_sig.Bool
-module NumerorsDomain: Parameter_sig.Bool
-module TracesDomain: Parameter_sig.Bool
-
-module ApronOctagon: Parameter_sig.Bool
-module ApronBox: Parameter_sig.Bool
-module PolkaLoose: Parameter_sig.Bool
-module PolkaStrict: Parameter_sig.Bool
-module PolkaEqualities: Parameter_sig.Bool
-
module EqualityCall: Parameter_sig.String
module EqualityCallFunction:
Parameter_sig.Map with type key = Cil_types.kernel_function
@@ -245,12 +227,6 @@ val dkey_widening : category
(** Registers available domain names for the -eva-domains option. *)
val register_domain: name:string -> descr:string -> unit
-(** Notifies that the binding to Apron domains is available. *)
-val register_apron: unit -> unit
-
-(** Notifies that the numerors domain is available. *)
-val register_numerors: unit -> unit
-
(*
Local Variables:
compile-command: "make -C ../../.."