diff --git a/src/plugins/e-acsl/src/analyses/bound_variables.ml b/src/plugins/e-acsl/src/analyses/bound_variables.ml index dcb33722d91302621808ce98e20c6ebc9858fe00..dedfa6fbbdf372091b1266509610bdfa108fbabe 100644 --- a/src/plugins/e-acsl/src/analyses/bound_variables.ml +++ b/src/plugins/e-acsl/src/analyses/bound_variables.ml @@ -36,8 +36,7 @@ open Cil_types open Cil_datatype open Error_types -module Error = - Error.Make(struct let phase = Options.register_category "bound variables" end) +module Error = Error.Make(struct let phase = Options.dkey_bound_variables end) (** [error_msg quantif msg pp x] creates an error message from the string [msg] containing the value [x] pretty-printed by [pp] and the predicate [quantif] diff --git a/src/plugins/e-acsl/src/analyses/interval.ml b/src/plugins/e-acsl/src/analyses/interval.ml index e22889902aaf7998ffd7d65caea3cc92f1ca482d..91ae17457801e9d52e389524a4f1e1d2ded96c1b 100644 --- a/src/plugins/e-acsl/src/analyses/interval.ml +++ b/src/plugins/e-acsl/src/analyses/interval.ml @@ -26,10 +26,7 @@ open Cil_types devenir plus rapide, plus précis et plus mince". Also implements a support for real numbers. *) -module Error = - Error.Make(struct - let phase = Options.register_category "interval inference" - end) +module Error = Error.Make(struct let phase = Options.dkey_interval end) (* ********************************************************************* *) (* Basic datatypes and operations *) diff --git a/src/plugins/e-acsl/src/analyses/memory_tracking.ml b/src/plugins/e-acsl/src/analyses/memory_tracking.ml index 8198d36429ca3f32d536b70c5324dcfb5817bab6..7e09d537bfcd9e20d3c893c7b0d12462c623f147 100644 --- a/src/plugins/e-acsl/src/analyses/memory_tracking.ml +++ b/src/plugins/e-acsl/src/analyses/memory_tracking.ml @@ -25,8 +25,8 @@ open Cil_datatype module Dataflow = Dataflow2 -module Error = - Error.Make(struct let phase = Options.register_category "memory tracking" end) +let dkey = Options.dkey_mtracking +module Error = Error.Make(struct let phase = dkey end) let must_never_monitor vi = (* E-ACSL, please do not monitor yourself! *) @@ -45,7 +45,6 @@ let must_never_monitor vi = left-values must be tracked by the memory model library *) (* ********************************************************************** *) -let dkey = Options.dkey_analysis module Env: sig val has_heap_allocations: unit -> bool val check_heap_allocations: kernel_function -> unit diff --git a/src/plugins/e-acsl/src/analyses/typing.ml b/src/plugins/e-acsl/src/analyses/typing.ml index a15b56b7caf2c3714ea1d83af9415dde86236c70..cc09eed3acbafac5a0a04555a331065707002cdf 100644 --- a/src/plugins/e-acsl/src/analyses/typing.ml +++ b/src/plugins/e-acsl/src/analyses/typing.ml @@ -27,7 +27,6 @@ open Error_types devenir plus rapide, plus précis et plus mince". *) let dkey = Options.dkey_typing - module Error = Error.Make(struct let phase = dkey end) (* In order to properly handle recursive functions the typing method has to diff --git a/src/plugins/e-acsl/src/options.ml b/src/plugins/e-acsl/src/options.ml index 3aa05ca87e7c9a344e71eaad8dfcb5ca1759cfd1..4b0313f0a0da5016ed63d11c20eb3a6e2836417b 100644 --- a/src/plugins/e-acsl/src/options.ml +++ b/src/plugins/e-acsl/src/options.ml @@ -172,10 +172,12 @@ let emitter = let must_visit () = Run.get () -let dkey_analysis = register_category "analysis" let dkey_prepare = register_category "preparation" +let dkey_bound_variables = register_category "analysis:bound_variables" +let dkey_interval = register_category "analysis:interval_inference" +let dkey_mtracking = register_category "analysis:memory_tracking" +let dkey_typing = register_category "analysis:typing" let dkey_translation = register_category "translation" -let dkey_typing = register_category "typing" let setup ?(rtl=false) () = (* Variadic translation *) diff --git a/src/plugins/e-acsl/src/options.mli b/src/plugins/e-acsl/src/options.mli index 3274f5591f038349c5ff4543435049566e33a153..ef70ed655ab8f0185322ff201f6efe5b46785d33 100644 --- a/src/plugins/e-acsl/src/options.mli +++ b/src/plugins/e-acsl/src/options.mli @@ -41,10 +41,12 @@ val emitter: Emitter.t val must_visit: unit -> bool -val dkey_analysis: category val dkey_prepare: category -val dkey_translation: category +val dkey_bound_variables: category +val dkey_interval: category +val dkey_mtracking: category val dkey_typing: category +val dkey_translation: category val setup: ?rtl:bool -> unit -> unit (** Verify and initialize the options of the current project according to the