diff --git a/src/plugins/e-acsl/Makefile.in b/src/plugins/e-acsl/Makefile.in
index fcc691668051214de6f8e7929ca59cbb9f971663..9a3630f170cc66ab7cd04ec1a7f6daa99dd3bbbc 100644
--- a/src/plugins/e-acsl/Makefile.in
+++ b/src/plugins/e-acsl/Makefile.in
@@ -79,6 +79,7 @@ CODE_GENERATOR_CMI:= \
CODE_GENERATOR_CMI:=$(addprefix src/code_generator/, $(CODE_GENERATOR_CMI))
SRC_CODE_GENERATOR:= \
+ translation_error \
smart_exp \
smart_stmt \
gmp \
diff --git a/src/plugins/e-acsl/headers/header_spec.txt b/src/plugins/e-acsl/headers/header_spec.txt
index 1b55d131f14c53ec0267cd93de192867d7315d9e..8c02f1e8c9dd2373e19f96f62113187f03701a66 100644
--- a/src/plugins/e-acsl/headers/header_spec.txt
+++ b/src/plugins/e-acsl/headers/header_spec.txt
@@ -145,6 +145,8 @@ src/code_generator/translate_terms.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/code_generator/translate_terms.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/code_generator/translate_utils.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/code_generator/translate_utils.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
+src/code_generator/translation_error.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
+src/code_generator/translation_error.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/code_generator/typed_number.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/code_generator/typed_number.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/libraries/builtins.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
diff --git a/src/plugins/e-acsl/src/analyses/bound_variables.ml b/src/plugins/e-acsl/src/analyses/bound_variables.ml
index 47f1d190eedefe4da58fbda750efe87e2c171511..dcb33722d91302621808ce98e20c6ebc9858fe00 100644
--- a/src/plugins/e-acsl/src/analyses/bound_variables.ml
+++ b/src/plugins/e-acsl/src/analyses/bound_variables.ml
@@ -36,6 +36,9 @@ open Cil_types
open Cil_datatype
open Error_types
+module Error =
+ Error.Make(struct let phase = Options.register_category "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]
pretty-printed. *)
@@ -688,11 +691,11 @@ end
| Pforall _ ->
Quantifier.add
p
- (Err (Error.Not_yet "unguarded \\forall quantification"))
+ (Err (Error.make_not_yet "unguarded \\forall quantification"))
| Pexists _ ->
Quantifier.add
p
- (Err (Error.Not_yet "unguarded \\exists quantification"))
+ (Err (Error.make_not_yet "unguarded \\exists quantification"))
| _ -> ()
let do_user_predicates () =
diff --git a/src/plugins/e-acsl/src/analyses/interval.ml b/src/plugins/e-acsl/src/analyses/interval.ml
index 42c19e2aeb1608d5a68bfc6db6dc259fd93a7ba8..e22889902aaf7998ffd7d65caea3cc92f1ca482d 100644
--- a/src/plugins/e-acsl/src/analyses/interval.ml
+++ b/src/plugins/e-acsl/src/analyses/interval.ml
@@ -26,6 +26,11 @@ 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)
+
(* ********************************************************************* *)
(* 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 dc76e43c7502f4b9620545f9108048f09939b646..8198d36429ca3f32d536b70c5324dcfb5817bab6 100644
--- a/src/plugins/e-acsl/src/analyses/memory_tracking.ml
+++ b/src/plugins/e-acsl/src/analyses/memory_tracking.ml
@@ -25,6 +25,9 @@ open Cil_datatype
module Dataflow = Dataflow2
+module Error =
+ Error.Make(struct let phase = Options.register_category "memory tracking" end)
+
let must_never_monitor vi =
(* E-ACSL, please do not monitor yourself! *)
Rtl.Symbols.mem_vi vi.vname
diff --git a/src/plugins/e-acsl/src/analyses/typing.ml b/src/plugins/e-acsl/src/analyses/typing.ml
index 6cd1e75891fdb7d263eccc484eaf7a6e90a97ec8..a15b56b7caf2c3714ea1d83af9415dde86236c70 100644
--- a/src/plugins/e-acsl/src/analyses/typing.ml
+++ b/src/plugins/e-acsl/src/analyses/typing.ml
@@ -28,6 +28,8 @@ open Error_types
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
store the result of the fixpoint algorithm on intervals before typing
the inner block of the function. To this end, we stop the recursive
diff --git a/src/plugins/e-acsl/src/code_generator/contract.ml b/src/plugins/e-acsl/src/code_generator/contract.ml
index df7029c708d9f9bd2c0600a1395fa0e8ea961d44..4a94572f472fa919d74158839eb92b4bca9d1c9d 100644
--- a/src/plugins/e-acsl/src/code_generator/contract.ml
+++ b/src/plugins/e-acsl/src/code_generator/contract.ml
@@ -22,6 +22,7 @@
open Cil_types
open Contract_types
+module Error = Translation_error
(**************************************************************************)
(********************** Contract ********************************)
diff --git a/src/plugins/e-acsl/src/code_generator/env.ml b/src/plugins/e-acsl/src/code_generator/env.ml
index 728c432a7c01a973e51aff0d881a7867021d227f..9e9404a854acc1296d087e6f9c55521d331b99da 100644
--- a/src/plugins/e-acsl/src/code_generator/env.ml
+++ b/src/plugins/e-acsl/src/code_generator/env.ml
@@ -24,6 +24,7 @@ module E_acsl_label = Label
open Cil_types
open Cil_datatype
open Contract_types
+module Error = Translation_error
type localized_scope =
| LGlobal
diff --git a/src/plugins/e-acsl/src/code_generator/gmp.ml b/src/plugins/e-acsl/src/code_generator/gmp.ml
index ff03f6e50bff630778283cb9a8c5b9396ee27880..2079c7e5ff2aa791d7ba89f81c8d40e07f849a1c 100644
--- a/src/plugins/e-acsl/src/code_generator/gmp.ml
+++ b/src/plugins/e-acsl/src/code_generator/gmp.ml
@@ -21,6 +21,7 @@
(**************************************************************************)
open Cil_types
+module Error = Translation_error
(**************************************************************************)
(************************* Calls to builtins ******************************)
diff --git a/src/plugins/e-acsl/src/code_generator/injector.ml b/src/plugins/e-acsl/src/code_generator/injector.ml
index 1ed98db412af31123e386f09d3df7fe5b1d9952e..e2c2362364258888ab87c59aac61de116d9ff419 100644
--- a/src/plugins/e-acsl/src/code_generator/injector.ml
+++ b/src/plugins/e-acsl/src/code_generator/injector.ml
@@ -23,6 +23,7 @@
module E_acsl_label = Label (* [Label] is hidden when opening [Cil_datatype *)
open Cil_types
open Cil_datatype
+module Error = Translation_error
let dkey = Options.dkey_translation
diff --git a/src/plugins/e-acsl/src/code_generator/label.ml b/src/plugins/e-acsl/src/code_generator/label.ml
index 7a3ae98c22e89831fec011763bb0f98eaf626f6d..f94d6294cba6921f9442420a4e86a056e981b9d3 100644
--- a/src/plugins/e-acsl/src/code_generator/label.ml
+++ b/src/plugins/e-acsl/src/code_generator/label.ml
@@ -21,6 +21,7 @@
(**************************************************************************)
open Cil_types
+module Error = Translation_error
(* The keys are the stmts which were previously labeled, whereas the associated
values are the new stmts containing the same labels. *)
diff --git a/src/plugins/e-acsl/src/code_generator/logic_functions.ml b/src/plugins/e-acsl/src/code_generator/logic_functions.ml
index bf606c9c4e3f029ad93c118fd9d335ce00ae980e..396a60a119ea184373f456e2f09fb1a5773f3601 100644
--- a/src/plugins/e-acsl/src/code_generator/logic_functions.ml
+++ b/src/plugins/e-acsl/src/code_generator/logic_functions.ml
@@ -22,6 +22,7 @@
open Cil_types
open Cil_datatype
+module Error = Translation_error
(**************************************************************************)
(********************** Forward references ********************************)
diff --git a/src/plugins/e-acsl/src/code_generator/memory_translate.ml b/src/plugins/e-acsl/src/code_generator/memory_translate.ml
index 561199aa97ed7d3679507d33a4a3ec381c4712d5..db33c80d423bb876503ae0823ff0ffc9c0d48469 100644
--- a/src/plugins/e-acsl/src/code_generator/memory_translate.ml
+++ b/src/plugins/e-acsl/src/code_generator/memory_translate.ml
@@ -21,6 +21,7 @@
(**************************************************************************)
open Cil_types
+module Error = Translation_error
(**************************************************************************)
(********************** Forward references ********************************)
diff --git a/src/plugins/e-acsl/src/code_generator/temporal.ml b/src/plugins/e-acsl/src/code_generator/temporal.ml
index 8e7c0b4123be95e27a9d22f56d14294703b73302..ee153ec4791f2d117e6c91c560ce5d80da97a537 100644
--- a/src/plugins/e-acsl/src/code_generator/temporal.ml
+++ b/src/plugins/e-acsl/src/code_generator/temporal.ml
@@ -27,6 +27,7 @@
module RTL = Functions.RTL
module Libc = Functions.Libc
+module Error = Translation_error
open Cil_types
open Cil_datatype
diff --git a/src/plugins/e-acsl/src/code_generator/translate_utils.ml b/src/plugins/e-acsl/src/code_generator/translate_utils.ml
index 5b7e7871488d30b22bdc6f9dd21a885c5e638402..318008a35cd5755589acd2ea88d043353de141a6 100644
--- a/src/plugins/e-acsl/src/code_generator/translate_utils.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate_utils.ml
@@ -25,6 +25,7 @@
module E_acsl_label = Label
open Cil_types
open Cil_datatype
+module Error = Translation_error
(**************************************************************************)
(********************** Forward references ********************************)
diff --git a/src/plugins/e-acsl/src/code_generator/translation_error.ml b/src/plugins/e-acsl/src/code_generator/translation_error.ml
new file mode 100644
index 0000000000000000000000000000000000000000..e4cd75f58e383eef0b75ad852c7c15ad2d8fd358
--- /dev/null
+++ b/src/plugins/e-acsl/src/code_generator/translation_error.ml
@@ -0,0 +1,23 @@
+(**************************************************************************)
+(* *)
+(* This file is part of the Frama-C's E-ACSL plug-in. *)
+(* *)
+(* Copyright (C) 2012-2021 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+include Error.Make(struct let phase = Options.dkey_translation end)
diff --git a/src/plugins/e-acsl/src/code_generator/translation_error.mli b/src/plugins/e-acsl/src/code_generator/translation_error.mli
new file mode 100644
index 0000000000000000000000000000000000000000..24208ba225d372a1a1232b30827c5ef5ee7fe70b
--- /dev/null
+++ b/src/plugins/e-acsl/src/code_generator/translation_error.mli
@@ -0,0 +1,23 @@
+(**************************************************************************)
+(* *)
+(* This file is part of the Frama-C's E-ACSL plug-in. *)
+(* *)
+(* Copyright (C) 2012-2021 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+include Error.S