diff --git a/doc/value/examples/parametrizing/makefile b/doc/value/examples/parametrizing/makefile index c4df2b77f47967aadce046cf1b74d69149f2a296..3a3b2ee42d80ae0d87a40f96084430b9f73e4d01 100644 --- a/doc/value/examples/parametrizing/makefile +++ b/doc/value/examples/parametrizing/makefile @@ -38,4 +38,4 @@ context-depth.3.log: FCFLAGS += -context-width 1 -context-depth 1 -context-valid slevel.1.log: FCFLAGS += -slevel 55 slevel.2.log: FCFLAGS += -slevel 28 ilevel.2.log: FCFLAGS += -val-ilevel 16 -split-fabs.log: FCFLAGS += -eva-equality-domain +split-fabs.log: FCFLAGS += -eva-domains equality diff --git a/doc/value/examples/parametrizing/out-of-bound.log b/doc/value/examples/parametrizing/out-of-bound.log index 365e3edd937c7a33c60cbe1bb5381abda8849cb9..b6d42e75c762d0b06d1c4b301e249cd373c1ce52 100644 --- a/doc/value/examples/parametrizing/out-of-bound.log +++ b/doc/value/examples/parametrizing/out-of-bound.log @@ -13,7 +13,7 @@ NON TERMINATING FUNCTION [eva:summary] ====== ANALYSIS SUMMARY ====== ---------------------------------------------------------------------------- - 1 function analyzed (out of 2): 50% coverage. + 1 function analyzed (out of 1): 100% coverage. In this function, 1 statements reached (out of 2): 50% coverage. ---------------------------------------------------------------------------- No errors or warnings raised during the analysis. diff --git a/doc/value/main.tex b/doc/value/main.tex index abb6737522fbfad435bb1ad7827f77e80a0dbe01..6a79827826a2eec15b5f907e931fe61de45fa91c 100644 --- a/doc/value/main.tex +++ b/doc/value/main.tex @@ -3740,7 +3740,7 @@ comparison like in the following example. \lstinputlisting{examples/parametrizing/split-fabs.c} This example requires the equality domain (enabled with option -\lstinline|-eva-equality-domain|, see section \ref{sec:symbolic-equalities}) to +\lstinline|-eva-domains equality|, see section \ref{sec:symbolic-equalities}) to be analyzed precisely, as we need the equality relations between the input and the output of the function \lstinline|fabs|, i.e. the relations \lstinline|x == \result| or \lstinline|x == -\result|. @@ -3849,6 +3849,10 @@ available to improve the precision on specific code constructs. They can (and probably should) be enabled at the beginning of the analysis. Their only downside is that they increase the analysis time. +These analysis domains are enabled by the option \texttt{-eva-domains}, followed +by a list of domain names. A list of the available domains, and a short +description of each one, can be displayed with \texttt{-eva-domains help}. + \emph{Restrictions:} \begin{itemize} \item adding a new domain may interact with the \lstinline+slevel+ partitioning @@ -3867,7 +3871,7 @@ categories are described in Section~\ref{buitins_observation}. \subsection{Symbolic equalities} \label{sec:symbolic-equalities} -Activating option \texttt{-eva-equality-domain} instructs +Activating option \texttt{-eva-domains equality} instructs \Eva{} to perform a special analysis that stores information about equalities found in the code. Those equalities may stem either from conditions (e.g. \texttt{if (x == y+1)}), or assignments @@ -3910,7 +3914,7 @@ Three global modes are available: \subsection{Reused left-values} \label{sec:reuse} -Activating option \texttt{-eva-symbolic-locations-domain} instructs +Activating option \texttt{-eva-domains symbolic-locations} instructs \Eva{} to perform a special analysis for \emph{reused left-values}. \begin{lstlisting} @@ -3943,7 +3947,7 @@ in the caller is not propagated in the callee. \subsection{Gauges} \label{sec:gauges} -Activating option \texttt{-eva-gauges-domain} instructs \Eva{} to +Activating option \texttt{-eva-domains gauges} instructs \Eva{} to store relations between integer (or pointer) variables modified by a loop, and the number of elapsed loop iterations. It is based on the paper \emph{``The Gauge Domain: Scalable Analysis of Linear @@ -4009,7 +4013,7 @@ and \texttt{y} is not affine. \subsection{Octagons} \label{sec:octagons} -Activating option \texttt{-eva-octagon-domain} instructs Eva to infer relations +Activating option \texttt{-eva-domains octagon} instructs Eva to infer relations between variables as numerical constraints of the form $l \leq \pm X \pm Y \leq u$, where $X$ and $Y$ are program variables, and $l$ and $u$ are constants. @@ -4059,7 +4063,7 @@ and at the end, the inferred relations are propagated back to the caller. \emph{This analysis is experimental.} -Activating option \texttt{-eva-bitwise-domain} instructs \Eva{} to store +Activating option \texttt{-eva-domains bitwise} instructs \Eva{} to store bitwise information in complement to the usual, interval-based, information. This is mostly useful for programs that use bitwise operators: \verb+&+, \verb+|+, \verb+^+ and \verb+~+, especially with bit-masks constants. @@ -4123,7 +4127,7 @@ in very long analyses and/or massive memory usage. \Eva{} provides a domain inferring ranges for the absolute and relative errors stemming from floating-point computations. This domain can be enabled by the -option \texttt{-eva-numerors-domain}. The theory and core principles underlying +option \texttt{-eva-domains numerors}. The theory and core principles underlying this domain are described in \cite{DBLP:conf/sas/JacqueminPV18}. The errors inferred by the domain can be seen in the GUI, alongside the other diff --git a/src/plugins/value/domains/apron/apron_domain.ml b/src/plugins/value/domains/apron/apron_domain.ml index d978ca8f1360b3b3c3496d112475df6b0a32da98..8915d40c396f57aaf97140bb23e241066397d70f 100644 --- a/src/plugins/value/domains/apron/apron_domain.ml +++ b/src/plugins/value/domains/apron/apron_domain.ml @@ -726,28 +726,24 @@ 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 = - "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 ~enable { 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 () + let abstraction = + Abstractions.{ values = Single (module Main_values.Interval); + domain = Domain (module Domain); } + in + Abstractions.register ~name ~descr ~experimental:true ~priority:1 abstraction +let octagon = make "octagon" (module Apron_Octagon) +let box = make "box" (module Apron_Box) +let polka_loose = make "polka-loose" (module Apron_Polka_Loose) +let polka_strict = make "polka-strict" (module Apron_Polka_Strict) +let polka_equality = make "polka-equality" (module Apron_Polka_Equalities) (* Local Variables: diff --git a/src/plugins/value/domains/apron/apron_domain.mli b/src/plugins/value/domains/apron/apron_domain.mli index 3ce613a2e4cb72a0c975be1dd1e953f51785a556..24703ead6f16909ec84f3ec840806cf297f2fee7 100644 --- a/src/plugins/value/domains/apron/apron_domain.mli +++ b/src/plugins/value/domains/apron/apron_domain.mli @@ -24,6 +24,12 @@ the APRON library: http://apron.cri.ensmp.fr/library For now, this binding only processes scalar integer variables. *) +val octagon: Abstractions.flag +val box: Abstractions.flag +val polka_loose: Abstractions.flag +val polka_strict: Abstractions.flag +val polka_equality: Abstractions.flag + (* Local Variables: compile-command: "make -C ../../../.." diff --git a/src/plugins/value/domains/numerors/numerors_domain.ml b/src/plugins/value/domains/numerors/numerors_domain.ml index b7d3142cede4d5a7c03cbdbc7f238da811ffb759..6fe3f9da06ad0730570a32512d780c7de505d3ea 100644 --- a/src/plugins/value/domains/numerors/numerors_domain.ml +++ b/src/plugins/value/domains/numerors/numerors_domain.ml @@ -153,16 +153,15 @@ let reduce_cast (module Abstract: Abstractions.S) = (* Register the domain as an Eva abstractions. *) 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); + let name = "numerors" + and descr = "Infers ranges for the absolute and relative errors \ + in floating-point computations. No support of loops." + and experimental = true + and abstraction = + { values = Single (module Numerors_value); 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; + ignore (register ~name ~descr ~experimental abstraction); 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..d393a2061409a669a59d45d703814d192735d35f 100644 --- a/src/plugins/value/engine/abstractions.ml +++ b/src/plugins/value/engine/abstractions.ml @@ -39,17 +39,20 @@ type 'v domain = | Functor: (module domain_functor) -> _ domain type 'v abstraction = + { values: 'v value; + domain: 'v domain; } + +type 't with_info = { name: string; - descr: string; + experimental: bool; priority: int; - values: 'v value; - domain: 'v domain; } + abstraction: 't; } + +type flag = Flag: 'v abstraction with_info -> flag (* --- Config and registration ---------------------------------------------- *) module Config = struct - type flag = Flag: 'v abstraction -> flag - module Flag = struct type t = flag @@ -61,104 +64,109 @@ module Config = struct include Set.Make (Flag) - type dynamic = Dynamic: (unit -> 'a option) * ('a -> 'v abstraction) -> dynamic + type dynamic = Dynamic: (unit -> 'v abstraction) with_info -> dynamic let abstractions = ref [] let dynamic_abstractions : dynamic list ref = ref [] - let register ~enable abstraction = - let { name; descr; } = abstraction in + let register ~name ~descr ?(experimental=false) ?(priority=0) abstraction = + let descr = if experimental then "Experimental. " ^ descr else descr in Value_parameters.register_domain ~name ~descr; - abstractions := (enable, Flag abstraction) :: !abstractions + let flag = Flag { name; experimental; priority; abstraction } in + abstractions := flag :: !abstractions; + flag - let dynamic_register ~configure ~make = - dynamic_abstractions := Dynamic (configure, make) :: !dynamic_abstractions + let dynamic_register ~name ~descr ?(experimental=false) ?(priority=0) make = + let descr = if experimental then "Experimental. " ^ descr else descr in + Value_parameters.register_domain ~name ~descr; + let dynamic = Dynamic { name; experimental; priority; abstraction=make; } in + dynamic_abstractions := dynamic :: !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 let config = List.fold_left aux empty !abstractions in - let aux config (Dynamic (configure, make)) = - match configure () with - | None -> config - | Some c -> add (Flag (make c)) config + let aux config (Dynamic { name; experimental; priority; abstraction; }) = + if Value_parameters.Domains.mem name + then + let abstraction = abstraction () in + let flag = Flag { name; experimental; priority; abstraction; } in + add flag config + else config in List.fold_left aux config !dynamic_abstractions (* --- Register default abstractions -------------------------------------- *) - let create ~enable abstract = register ~enable abstract; Flag abstract - let create_domain priority name descr enable values domain = - create ~enable - { name; descr; priority; values = Single values; domain = Domain domain } - - open Value_parameters + let create_domain ?experimental priority name descr values domain = + let abstraction = { values = Single values; domain = Domain domain } in + register ~name ~descr ~priority ?experimental abstraction (* Register standard domains over cvalues. *) - let make rank name descr enable = - create_domain rank name descr enable (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" "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) - - 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 + (module Symbolic_locs.D) + + let equality = + let descr = "Infers equalities between syntactic C expressions. \ + Makes the analysis less dependent on temporary variables and \ + intermediate computations." + and abstraction = + { values = Struct Abstract.Value.Unit; + domain = Functor (module Equality_domain.Make); } + in + register ~name:"equality" ~descr ~priority:8 abstraction 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) + 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." - 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 ---------------------------------- *) @@ -223,8 +231,8 @@ module Internal_Value = struct aux value internal let build_values config initial_value = - let build (Config.Flag abstraction) acc = - match abstraction.values with + let build (Flag flag) acc = + match flag.abstraction.values with | Struct structure -> add_value_structure acc structure | Single (module V) -> add_value_leaf acc (V (V.key, (module V))) in @@ -323,8 +331,16 @@ let add_domain (type v) (abstraction: v abstraction) (module Acc: Acc) = module Dom = (val domain) end : Acc) +let warn_experimental flag = + if flag.experimental then + Value_parameters.(warning ~wkey:wkey_experimental + "The %s domain is experimental." flag.name) + let build_domain config abstract = - let build (Config.Flag abstraction) acc = add_domain abstraction acc in + let build (Flag flag) acc = + warn_experimental flag; + add_domain flag.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 9ccac22fb48203b2bcf5ce06292a52c55da862b6..0156b516d8ad4b0e39cdad5baaa1986a5547e08b 100644 --- a/src/plugins/value/engine/abstractions.mli +++ b/src/plugins/value/engine/abstractions.mli @@ -56,32 +56,47 @@ type 'v domain = | Domain: (module leaf_domain with type value = 'v) -> '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. *) +(** Abstraction to be registered. *) 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. *) + { 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 - [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 +(** Information about a registered abstraction. *) +type 't with_info = + { name: string; (** Name of the domain. Must be unique. *) + experimental: bool; (** Is the domain experimental? *) + priority: int; (** Domains with higher priority are processed first. *) + abstraction: 't; (** The abstract value and the domain. *) + } + +(** Flag for an abstract domain. A domain can be programmatically enabled via + its flag. See module {!Config} for more details. *) +type flag = Flag: 'v abstraction with_info -> flag + +(** Registers an abstract domain. Returns a flag for the given domain. + - [name] must be unique. The domain is used if the -eva-domains option + has been set to [name]. + - [descr] is a description printed in the help message of -eva-domains. + - [experimental] is false by default. If set to true, a warning is emitted + when the domain is enabled. + - [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. The default priority is 0. *) +val register: + name:string -> descr:string -> ?experimental:bool -> ?priority:int -> + 'v abstraction -> flag (** Register a dynamic abstraction: the abstraction is built by applying - [make (configure ())] at the start of each analysis. *) + the last argument when starting an analysis, if the -eva-domains option + has been set to [name]. See function {!register} for more details. *) val dynamic_register: - configure:(unit -> 'a option) -> make:('a -> 'v abstraction) -> unit + name:string -> descr:string -> ?experimental:bool -> ?priority:int -> + (unit -> 'v abstraction) -> unit -(** Value reduced product between two value abstractions, identified by their - keys. *) +(** Reduced product between two value abstractions, identified by their keys. *) type ('a, 'b) value_reduced_product = 'a Abstract.Value.key * 'b Abstract.Value.key * ('a -> 'b -> 'a * 'b) @@ -121,12 +136,9 @@ val register_hook: ((module S) -> (module S)) -> unit (** {2 Configuration of an analysis.} *) -(** Configuration defining the abstractions to be used in an analysis. *) +(** Configuration defining the abstractions to be used in an analysis. + A configuration is a set of flags, i.e. a set of enabled abstractions. *) module Config : sig - (** Flag for an abstraction. *) - type flag = Flag: 'v abstraction -> flag - - (** A configuration is a set of flags, i.e. a set of enabled abstractions. *) include Set.S with type elt = flag (** Flags for the standard domains currently provided in Eva. *) diff --git a/src/plugins/value/value_parameters.ml b/src/plugins/value/value_parameters.ml index 4ee2d35357174a64eabd0596aa4e4329a16ea136..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 @@ -126,14 +125,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 +188,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 +211,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 +1471,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 +1497,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..bca2258cec9aff02f34e07b6822e58a0fd109799 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 @@ -221,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 @@ -245,12 +230,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 ../../.." diff --git a/tests/builtins/test_config_apron b/tests/builtins/test_config_apron index 98b3a98fc6861091dda33b4cbaca1a2ab5278d4c..e5aae7331927957a07fa55967355b78ed147f1b5 100644 --- a/tests/builtins/test_config_apron +++ b/tests/builtins/test_config_apron @@ -1,3 +1,3 @@ -MACRO: EVA_OPTIONS @EVA_OPTIONS@ -eva-msg-key malloc -eva-warn-key malloc:weak=feedback -eva-no-alloc-returns-null -eva-apron-oct -eva-msg-key experimental-ok +MACRO: EVA_OPTIONS @EVA_OPTIONS@ -eva-msg-key malloc -eva-warn-key malloc:weak=feedback -eva-no-alloc-returns-null MACRO: EVA_CONFIG @EVA_OPTIONS@ -no-autoload-plugins -load-module from,inout,eva,scope,variadic OPT: -eva @EVA_CONFIG@ -journal-disable -out -input -deps diff --git a/tests/builtins/test_config_bitwise b/tests/builtins/test_config_bitwise index fddf8d55557c30d3d3536b1356b1cfe9e85870ec..e5aae7331927957a07fa55967355b78ed147f1b5 100644 --- a/tests/builtins/test_config_bitwise +++ b/tests/builtins/test_config_bitwise @@ -1,3 +1,3 @@ -MACRO: EVA_OPTIONS @EVA_OPTIONS@ -eva-msg-key malloc -eva-warn-key malloc:weak=feedback -eva-no-alloc-returns-null -eva-bitwise-domain +MACRO: EVA_OPTIONS @EVA_OPTIONS@ -eva-msg-key malloc -eva-warn-key malloc:weak=feedback -eva-no-alloc-returns-null MACRO: EVA_CONFIG @EVA_OPTIONS@ -no-autoload-plugins -load-module from,inout,eva,scope,variadic OPT: -eva @EVA_CONFIG@ -journal-disable -out -input -deps diff --git a/tests/builtins/test_config_equalities b/tests/builtins/test_config_equalities index 6f71f51c4d9dc983af96581eb9517fa3b7db3be1..e5aae7331927957a07fa55967355b78ed147f1b5 100644 --- a/tests/builtins/test_config_equalities +++ b/tests/builtins/test_config_equalities @@ -1,3 +1,3 @@ -MACRO: EVA_OPTIONS @EVA_OPTIONS@ -eva-msg-key malloc -eva-warn-key malloc:weak=feedback -eva-no-alloc-returns-null -eva-equality-domain +MACRO: EVA_OPTIONS @EVA_OPTIONS@ -eva-msg-key malloc -eva-warn-key malloc:weak=feedback -eva-no-alloc-returns-null MACRO: EVA_CONFIG @EVA_OPTIONS@ -no-autoload-plugins -load-module from,inout,eva,scope,variadic OPT: -eva @EVA_CONFIG@ -journal-disable -out -input -deps diff --git a/tests/builtins/test_config_gauges b/tests/builtins/test_config_gauges index 3e142f5beb772fe8df5fd28fcfa52c0fa88ba49a..e5aae7331927957a07fa55967355b78ed147f1b5 100644 --- a/tests/builtins/test_config_gauges +++ b/tests/builtins/test_config_gauges @@ -1,3 +1,3 @@ -MACRO: EVA_OPTIONS @EVA_OPTIONS@ -eva-msg-key malloc -eva-warn-key malloc:weak=feedback -eva-no-alloc-returns-null -eva-gauges-domain +MACRO: EVA_OPTIONS @EVA_OPTIONS@ -eva-msg-key malloc -eva-warn-key malloc:weak=feedback -eva-no-alloc-returns-null MACRO: EVA_CONFIG @EVA_OPTIONS@ -no-autoload-plugins -load-module from,inout,eva,scope,variadic OPT: -eva @EVA_CONFIG@ -journal-disable -out -input -deps diff --git a/tests/builtins/test_config_octagons b/tests/builtins/test_config_octagons index 848a1c5fa4142125e0dc80808d0a8027d9760a2a..e5aae7331927957a07fa55967355b78ed147f1b5 100644 --- a/tests/builtins/test_config_octagons +++ b/tests/builtins/test_config_octagons @@ -1,3 +1,3 @@ -MACRO: EVA_OPTIONS @EVA_OPTIONS@ -eva-msg-key malloc -eva-warn-key malloc:weak=feedback -eva-no-alloc-returns-null -eva-octagon-domain +MACRO: EVA_OPTIONS @EVA_OPTIONS@ -eva-msg-key malloc -eva-warn-key malloc:weak=feedback -eva-no-alloc-returns-null MACRO: EVA_CONFIG @EVA_OPTIONS@ -no-autoload-plugins -load-module from,inout,eva,scope,variadic OPT: -eva @EVA_CONFIG@ -journal-disable -out -input -deps diff --git a/tests/builtins/test_config_symblocs b/tests/builtins/test_config_symblocs index f5dc3a45b44ea0dd7268899573566c797a79e336..e5aae7331927957a07fa55967355b78ed147f1b5 100644 --- a/tests/builtins/test_config_symblocs +++ b/tests/builtins/test_config_symblocs @@ -1,3 +1,3 @@ -MACRO: EVA_OPTIONS @EVA_OPTIONS@ -eva-msg-key malloc -eva-warn-key malloc:weak=feedback -eva-no-alloc-returns-null -eva-symbolic-locations-domain +MACRO: EVA_OPTIONS @EVA_OPTIONS@ -eva-msg-key malloc -eva-warn-key malloc:weak=feedback -eva-no-alloc-returns-null MACRO: EVA_CONFIG @EVA_OPTIONS@ -no-autoload-plugins -load-module from,inout,eva,scope,variadic OPT: -eva @EVA_CONFIG@ -journal-disable -out -input -deps diff --git a/tests/test_config_apron b/tests/test_config_apron index f2cc7c99925549ed501f9c2920742c71f2896639..9756305b89f7a2b23fb4e4ac2f85278695cfa612 100644 --- a/tests/test_config_apron +++ b/tests/test_config_apron @@ -1,3 +1,3 @@ -MACRO: EVA_OPTIONS -eva-show-progress -eva-msg-key=-summary -eva-auto-loop-unroll 0 -eva-apron-oct -eva-msg-key experimental-ok +MACRO: EVA_OPTIONS -eva-show-progress -eva-msg-key=-summary -eva-auto-loop-unroll 0 -eva-domains apron-octagon -eva-warn-key experimental=inactive MACRO: EVA_CONFIG @EVA_OPTIONS@ -no-autoload-plugins -load-module from,inout,eva,scope,variadic OPT: -eva @EVA_CONFIG@ -journal-disable -out -input -deps diff --git a/tests/test_config_bitwise b/tests/test_config_bitwise index 78b3b47c351dd5164adf860a4276680135700ccb..2de393bf539f8cf6a0e4b402b7693073f9b5fcc8 100644 --- a/tests/test_config_bitwise +++ b/tests/test_config_bitwise @@ -1,3 +1,3 @@ -MACRO: EVA_OPTIONS -eva-show-progress -eva-msg-key=-summary -eva-auto-loop-unroll 0 -eva-bitwise-domain +MACRO: EVA_OPTIONS -eva-show-progress -eva-msg-key=-summary -eva-auto-loop-unroll 0 -eva-domains bitwise MACRO: EVA_CONFIG @EVA_OPTIONS@ -no-autoload-plugins -load-module from,inout,eva,scope,variadic OPT: -eva @EVA_CONFIG@ -journal-disable -out -input -deps diff --git a/tests/test_config_equalities b/tests/test_config_equalities index c386ea89a05c577a7ce1ca5f9a01308c1b02948a..2758bbcdc4c9947e736388b45e175af3ab527c0f 100644 --- a/tests/test_config_equalities +++ b/tests/test_config_equalities @@ -1,3 +1,3 @@ -MACRO: EVA_OPTIONS -eva-show-progress -eva-msg-key=-summary -eva-auto-loop-unroll 0 -eva-equality-domain +MACRO: EVA_OPTIONS -eva-show-progress -eva-msg-key=-summary -eva-auto-loop-unroll 0 -eva-domains equality MACRO: EVA_CONFIG @EVA_OPTIONS@ -no-autoload-plugins -load-module from,inout,eva,scope,variadic OPT: -eva @EVA_CONFIG@ -journal-disable -out -input -deps diff --git a/tests/test_config_gauges b/tests/test_config_gauges index bc7593f4e6be173da86718fce2727ad8c60be77e..9c8f47712455d77cef4f1985cbbb45e57cb572a4 100644 --- a/tests/test_config_gauges +++ b/tests/test_config_gauges @@ -1,3 +1,3 @@ -MACRO: EVA_OPTIONS -eva-show-progress -eva-msg-key=-summary -eva-auto-loop-unroll 0 -eva-gauges-domain +MACRO: EVA_OPTIONS -eva-show-progress -eva-msg-key=-summary -eva-auto-loop-unroll 0 -eva-domains gauges MACRO: EVA_CONFIG @EVA_OPTIONS@ -no-autoload-plugins -load-module from,inout,eva,scope,variadic OPT: -eva @EVA_CONFIG@ -journal-disable -out -input -deps diff --git a/tests/test_config_octagons b/tests/test_config_octagons index 701bc8421e733eb40844d0b62ab65400925c498e..27c9bcc81711c7516b7669081b30ee458cf29077 100644 --- a/tests/test_config_octagons +++ b/tests/test_config_octagons @@ -1,3 +1,3 @@ -MACRO: EVA_OPTIONS -eva-show-progress -eva-msg-key=-summary -eva-octagon-domain +MACRO: EVA_OPTIONS -eva-show-progress -eva-msg-key=-summary -eva-domains octagon MACRO: EVA_CONFIG @EVA_OPTIONS@ -no-autoload-plugins -load-module from,inout,eva,scope,variadic OPT: -eva @EVA_CONFIG@ -journal-disable -out -input -deps diff --git a/tests/test_config_symblocs b/tests/test_config_symblocs index 8cbbc295b177df03ddd9d2655b1bba2d2e68acde..c90d71b9e632ed8b8933b8ca2316b533858a0d27 100644 --- a/tests/test_config_symblocs +++ b/tests/test_config_symblocs @@ -1,3 +1,3 @@ -MACRO: EVA_OPTIONS -eva-show-progress -eva-msg-key=-summary -eva-auto-loop-unroll 0 -eva-symbolic-locations-domain +MACRO: EVA_OPTIONS -eva-show-progress -eva-msg-key=-summary -eva-auto-loop-unroll 0 -eva-domains symbolic-locations MACRO: EVA_CONFIG @EVA_OPTIONS@ -no-autoload-plugins -load-module from,inout,eva,scope,variadic OPT: -eva @EVA_CONFIG@ -journal-disable -out -input -deps diff --git a/tests/value/domains.i b/tests/value/domains.i index 4a1fe128ef255aedfd3a1ca2fe50bd7c2fbf7d03..434324fc2f5dd1047505aed2df088c06631bdccb 100644 --- a/tests/value/domains.i +++ b/tests/value/domains.i @@ -1,5 +1,5 @@ /* run.config* - STDOPT: #"-eva-sign-domain -eva-equality-domain -eva-bitwise-domain -eva-symbolic-locations-domain -eva-gauges-domain -slevel 2" + STDOPT: #"-eva-domains sign,equality,bitwise,symbolic-locations,gauges -slevel 2" */ /* Tests five domains together. */ diff --git a/tests/value/equality.c b/tests/value/equality.c index bbc36f8efbc4e41f11178ddbb46d23dc314619f4..c7c17cc1912cd5baa47a4fc1460c4fbfdeee823c 100644 --- a/tests/value/equality.c +++ b/tests/value/equality.c @@ -1,5 +1,5 @@ /* run.config* - STDOPT: +"-eva-equality-domain -eva-warn-copy-indeterminate=-assign_by_copy" + STDOPT: +"-eva-domains equality -eva-warn-copy-indeterminate=-assign_by_copy" */ /* Tests for the equality domain. */ diff --git a/tests/value/numerors/numerors.c b/tests/value/numerors/numerors.c index 6cd8c9573b7b9b004fbe1ee9d493d6e0130d9582..fd0609d1213af2c53e128e9dce2573823dc773df 100644 --- a/tests/value/numerors/numerors.c +++ b/tests/value/numerors/numerors.c @@ -1,5 +1,5 @@ /* run.config - OPT: -eva -eva-numerors-domain -eva-msg-key=d-numerors + OPT: -eva -eva-domains numerors -eva-msg-key=d-numerors */ /* Tests for the numerors domain, that computes absolute and relative errors diff --git a/tests/value/numerors/oracle/numerors.res.oracle b/tests/value/numerors/oracle/numerors.res.oracle index b6bde3cbebb23d7897c74e3661ee2ec094742a7a..96be7457bfd14f6f6707c210dea5bd6fd6bdb68a 100644 --- a/tests/value/numerors/oracle/numerors.res.oracle +++ b/tests/value/numerors/oracle/numerors.res.oracle @@ -1,4 +1,4 @@ -[eva] Warning: The numerors domain is experimental. +[eva:experimental] Warning: The numerors domain is experimental. [kernel] Parsing tests/value/numerors/numerors.c (with preprocessing) [kernel:parser:decimal-float] tests/value/numerors/numerors.c:24: Warning: Floating-point constant 0.69314718056 is not represented exactly. Will use 0x1.62e42fefa3bdcp-1. diff --git a/tests/value/octagons.c b/tests/value/octagons.c index 6d98523df71429efead57e87dd17633ea4ca4560..d1784f0eb4b39073fa9cfd69baa940411ded3484 100644 --- a/tests/value/octagons.c +++ b/tests/value/octagons.c @@ -1,5 +1,5 @@ /* run.config* - STDOPT: +" -eva-octagon-domain -eva-octagon-through-calls -eva-msg-key=d-octagon,-d-cvalue" + STDOPT: +" -eva-domains octagon -eva-octagon-through-calls -eva-msg-key=d-octagon,-d-cvalue" */ #include <__fc_builtin.h> diff --git a/tests/value/traces/oracle/test1.res.oracle b/tests/value/traces/oracle/test1.res.oracle index 679625f40788362b3bb3910df23bb974d38a6738..3d86f18943019f3f0a467294eb91a6e35ce14333 100644 --- a/tests/value/traces/oracle/test1.res.oracle +++ b/tests/value/traces/oracle/test1.res.oracle @@ -1,3 +1,4 @@ +[eva:experimental] Warning: The traces domain is experimental. [kernel] Parsing tests/value/traces/test1.c (with preprocessing) [eva] Analyzing a complete application starting at main [eva] Computing initial state diff --git a/tests/value/traces/oracle/test2.res.oracle b/tests/value/traces/oracle/test2.res.oracle index 65c109933939b95fb5d020721e76de0b4dc550a6..200e815eb5c348b65cc3bb4411ebf9401052ac21 100644 --- a/tests/value/traces/oracle/test2.res.oracle +++ b/tests/value/traces/oracle/test2.res.oracle @@ -1,3 +1,4 @@ +[eva:experimental] Warning: The traces domain is experimental. [kernel] Parsing tests/value/traces/test2.i (no preprocessing) [eva] Analyzing a complete application starting at main [eva] Computing initial state diff --git a/tests/value/traces/oracle/test3.res.oracle b/tests/value/traces/oracle/test3.res.oracle index 94615aa1fd40d461d21b8914fbc9490ccf004a56..1557613f54517aa6adcf22b46a8b6f617191eff7 100644 --- a/tests/value/traces/oracle/test3.res.oracle +++ b/tests/value/traces/oracle/test3.res.oracle @@ -1,3 +1,4 @@ +[eva:experimental] Warning: The traces domain is experimental. [kernel] Parsing tests/value/traces/test3.i (no preprocessing) [eva] Analyzing a complete application starting at main [eva] Computing initial state diff --git a/tests/value/traces/oracle/test4.res.oracle b/tests/value/traces/oracle/test4.res.oracle index 131cdfb303e054a35f2fc4f8e90c97fdbcaedb83..ffd3f1dd1ce713fc3f9efc6ac926cd892952e725 100644 --- a/tests/value/traces/oracle/test4.res.oracle +++ b/tests/value/traces/oracle/test4.res.oracle @@ -1,3 +1,4 @@ +[eva:experimental] Warning: The traces domain is experimental. [kernel] Parsing tests/value/traces/test4.i (no preprocessing) [eva] Analyzing a complete application starting at main [eva] Computing initial state diff --git a/tests/value/traces/oracle/test5.res.oracle b/tests/value/traces/oracle/test5.res.oracle index 815b9a52bd370ee6179be96c05a8b4a23601ab60..0715058c74b454795f3d2ddd083afeb84b532d2f 100644 --- a/tests/value/traces/oracle/test5.res.oracle +++ b/tests/value/traces/oracle/test5.res.oracle @@ -1,3 +1,4 @@ +[eva:experimental] Warning: The traces domain is experimental. [kernel] Parsing tests/value/traces/test5.i (no preprocessing) [kernel:typing:implicit-function-declaration] tests/value/traces/test5.i:21: Warning: Calling undeclared function my_switch. Old style K&R code? diff --git a/tests/value/traces/test1.c b/tests/value/traces/test1.c index 7fbd4347cc727b620b12ca1b06733b6ec3dbf427..b6097db5d277c05f882ffbd7b5794ca3be9eaf55 100644 --- a/tests/value/traces/test1.c +++ b/tests/value/traces/test1.c @@ -1,5 +1,5 @@ /* run.config - STDOPT: #"-eva-traces-domain -value-msg-key d-traces -slevel 10 -eva-traces-project" +"-then-last -val -print -value-msg-key=-d-traces" + STDOPT: #"-eva-domains traces -value-msg-key d-traces -slevel 10 -eva-traces-project" +"-then-last -val -print -value-msg-key=-d-traces" */ extern volatile int entropy_source; diff --git a/tests/value/traces/test2.i b/tests/value/traces/test2.i index 6369b92fd4c148354a6d23f5c80ec7b2cf5715ce..506b765112f7299a247614388e37f77a0529ca2e 100644 --- a/tests/value/traces/test2.i +++ b/tests/value/traces/test2.i @@ -1,5 +1,5 @@ /* run.config - STDOPT: #"-eva-traces-domain -value-msg-key d-traces -slevel 10 -eva-traces-project" +"-then-last -val -print -value-msg-key=-d-traces" + STDOPT: #"-eva-domains traces -value-msg-key d-traces -slevel 10 -eva-traces-project" +"-then-last -val -print -value-msg-key=-d-traces" */ diff --git a/tests/value/traces/test3.i b/tests/value/traces/test3.i index 6cd21d4315dfd93081a0edf0565c44b5aa093d30..80f30b09d39867dbe21a746c0ab0eb775ec9cc98 100644 --- a/tests/value/traces/test3.i +++ b/tests/value/traces/test3.i @@ -1,5 +1,5 @@ /* run.config - STDOPT: #"-eva-traces-domain -value-msg-key d-traces -slevel 10 -eva-traces-project" +"-then-last -val -print -value-msg-key=-d-traces" + STDOPT: #"-eva-domains traces -value-msg-key d-traces -slevel 10 -eva-traces-project" +"-then-last -val -print -value-msg-key=-d-traces" */ int g; diff --git a/tests/value/traces/test4.i b/tests/value/traces/test4.i index 9d4bc60920adba9604d26d492c44a55c77231b59..5cb5ad20e108eb43f8bd401375b2f9eaa8b35790 100644 --- a/tests/value/traces/test4.i +++ b/tests/value/traces/test4.i @@ -1,5 +1,5 @@ /* run.config - STDOPT: #"-eva-traces-domain -value-msg-key d-traces -slevel 10" + STDOPT: #"-eva-domains traces -value-msg-key d-traces -slevel 10" */ /* Test of join inside a loop */ diff --git a/tests/value/traces/test5.i b/tests/value/traces/test5.i index 046cafc651537cef93274c62a847157b4b495efd..60775951cadfd3c59496c198156438b766b3451e 100644 --- a/tests/value/traces/test5.i +++ b/tests/value/traces/test5.i @@ -1,5 +1,5 @@ /* run.config - STDOPT: #"-eva-traces-domain -value-msg-key d-traces -slevel 10" +"-then-last -val -slevel 10 -print -no-eva-traces-domain" + STDOPT: #"-eva-domains traces -value-msg-key d-traces -slevel 10" +"-then-last -val -slevel 10 -print -no-eva-traces-domain" */