From 16ae8e68ac47756cf64fa0e5ff4da3d0beb59924 Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Mon, 17 Jan 2022 15:34:07 +0100
Subject: [PATCH] [eacsl] Update error modules
---
src/plugins/e-acsl/Makefile.in | 1 +
src/plugins/e-acsl/headers/header_spec.txt | 2 ++
.../e-acsl/src/analyses/bound_variables.ml | 7 ++++--
src/plugins/e-acsl/src/analyses/interval.ml | 5 ++++
.../e-acsl/src/analyses/memory_tracking.ml | 3 +++
src/plugins/e-acsl/src/analyses/typing.ml | 2 ++
.../e-acsl/src/code_generator/contract.ml | 1 +
src/plugins/e-acsl/src/code_generator/env.ml | 1 +
src/plugins/e-acsl/src/code_generator/gmp.ml | 1 +
.../e-acsl/src/code_generator/injector.ml | 1 +
.../e-acsl/src/code_generator/label.ml | 1 +
.../src/code_generator/logic_functions.ml | 1 +
.../src/code_generator/memory_translate.ml | 1 +
.../e-acsl/src/code_generator/temporal.ml | 1 +
.../src/code_generator/translate_utils.ml | 1 +
.../src/code_generator/translation_error.ml | 23 +++++++++++++++++++
.../src/code_generator/translation_error.mli | 23 +++++++++++++++++++
17 files changed, 73 insertions(+), 2 deletions(-)
create mode 100644 src/plugins/e-acsl/src/code_generator/translation_error.ml
create mode 100644 src/plugins/e-acsl/src/code_generator/translation_error.mli
diff --git a/src/plugins/e-acsl/Makefile.in b/src/plugins/e-acsl/Makefile.in
index fcc69166805..9a3630f170c 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 1b55d131f14..8c02f1e8c9d 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 47f1d190eed..dcb33722d91 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 42c19e2aeb1..e22889902aa 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 dc76e43c750..8198d36429c 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 6cd1e75891f..a15b56b7caf 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 df7029c708d..4a94572f472 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 728c432a7c0..9e9404a854a 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 ff03f6e50bf..2079c7e5ff2 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 1ed98db412a..e2c23623642 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 7a3ae98c22e..f94d6294cba 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 bf606c9c4e3..396a60a119e 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 561199aa97e..db33c80d423 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 8e7c0b4123b..ee153ec4791 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 5b7e7871488..318008a35cd 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 00000000000..e4cd75f58e3
--- /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 00000000000..24208ba225d
--- /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
--
GitLab