From ed7d9f6f7e055d6bb18c136a140cff412b1d72eb Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Wed, 19 Jan 2022 11:30:13 +0100
Subject: [PATCH] =?UTF-8?q?REVUE=201=20:=20d=C3=A9claration=20des=20dkey?=
=?UTF-8?q?=20dans=20Options?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit
---
src/plugins/e-acsl/src/analyses/bound_variables.ml | 3 +--
src/plugins/e-acsl/src/analyses/interval.ml | 5 +----
src/plugins/e-acsl/src/analyses/memory_tracking.ml | 5 ++---
src/plugins/e-acsl/src/analyses/typing.ml | 1 -
src/plugins/e-acsl/src/options.ml | 6 ++++--
src/plugins/e-acsl/src/options.mli | 6 ++++--
6 files changed, 12 insertions(+), 14 deletions(-)
diff --git a/src/plugins/e-acsl/src/analyses/bound_variables.ml b/src/plugins/e-acsl/src/analyses/bound_variables.ml
index dcb33722d91..dedfa6fbbdf 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 e22889902aa..91ae1745780 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 8198d36429c..7e09d537bfc 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 a15b56b7caf..cc09eed3acb 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 3aa05ca87e7..4b0313f0a0d 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 3274f5591f0..ef70ed655ab 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
--
GitLab