diff --git a/src/plugins/e-acsl/E_ACSL.mli b/src/plugins/e-acsl/E_ACSL.mli
index 1b68985666fefd13c46a870f943d8e62705ccd83..d6d9aa9833290d36583e44637995e398d2fbe80e 100644
--- a/src/plugins/e-acsl/E_ACSL.mli
+++ b/src/plugins/e-acsl/E_ACSL.mli
@@ -24,9 +24,13 @@
open Cil_types
+module Options: sig
+ type category
+end
+
module Error: sig
- exception Typing_error of string
- exception Not_yet of string
+ exception Typing_error of Options.category option * string
+ exception Not_yet of Options.category option * string
end
module Translate_terms: sig
diff --git a/src/plugins/e-acsl/Makefile.in b/src/plugins/e-acsl/Makefile.in
index 25672c530b45fa6983742a093f233076eb1393e4..9adf75183d4d77db8012b6edffd3063eeb2d3fe3 100644
--- a/src/plugins/e-acsl/Makefile.in
+++ b/src/plugins/e-acsl/Makefile.in
@@ -39,6 +39,7 @@ endif
# libraries
SRC_LIBRARIES:= \
+ result \
error \
builtins \
functions \
@@ -75,6 +76,7 @@ CODE_GENERATOR_CMI:= \
CODE_GENERATOR_CMI:=$(addprefix src/code_generator/, $(CODE_GENERATOR_CMI))
SRC_CODE_GENERATOR:= \
+ translation_error \
smart_exp \
smart_stmt \
gmp \
@@ -126,6 +128,7 @@ PLUGIN_CMO:= src/local_config \
$(SRC_CODE_GENERATOR) \
src/main
PLUGIN_CMI:= \
+ $(LIBRARIES_CMI) \
$(CODE_GENERATOR_CMI)
PLUGIN_HAS_MLI:=yes
PLUGIN_DISTRIBUTED:=yes
diff --git a/src/plugins/e-acsl/headers/header_spec.txt b/src/plugins/e-acsl/headers/header_spec.txt
index 4c8e1b257363ff9294e43b8253cadbc90388bd94..0f167bcdc56cfba05508ea91ef7a3a08120781f5 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
@@ -159,6 +161,8 @@ src/libraries/logic_aggr.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/libraries/logic_aggr.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/libraries/misc.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/libraries/misc.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
+src/libraries/result.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
+src/libraries/result.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/libraries/varname.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/libraries/varname.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/local_config.mli: 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 11c3ece5c095329e507b8786548df158a0682dad..344736aa651363d15c8ebb2445f2f6a93a0f3a81 100644
--- a/src/plugins/e-acsl/src/analyses/bound_variables.ml
+++ b/src/plugins/e-acsl/src/analyses/bound_variables.ml
@@ -35,6 +35,8 @@
open Cil_types
open Cil_datatype
+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]
pretty-printed. *)
@@ -81,11 +83,11 @@ module Quantified_predicate =
module Quantifier: sig
val add:
predicate ->
- ((term * logic_var * term) list * predicate) Error.or_error ->
+ ((term * logic_var * term) list * predicate) Result.t ->
unit
val get:
predicate ->
- ((term * logic_var * term) list * predicate) Error.or_error
+ ((term * logic_var * term) list * predicate) Result.t
(** getter and setter for the additional guard that intersects with the type
of the variable *)
val get_guard_for_small_type : logic_var -> predicate option
@@ -113,7 +115,7 @@ end = struct
Cil_datatype.Logic_var.Hashtbl.add guard_tbl lv p
let replace p guarded_vars goal =
- Quantified_predicate.Hashtbl.replace tbl p (Error.Res (guarded_vars, goal))
+ Quantified_predicate.Hashtbl.replace tbl p (Result.Res (guarded_vars, goal))
let clear () =
Cil_datatype.Logic_var.Hashtbl.clear guard_tbl;
@@ -666,9 +668,9 @@ let compute_guards loc ~is_forall p bounded_vars hyps =
let guards,goal = compute_quantif_guards p ~is_forall bounded_vars hyps in
(* transform [guards] into [lscope_var list] *)
let normalized_guards = List.map (normalize_guard ~loc) guards
- in Quantifier.add p (Res (normalized_guards,goal))
+ in Quantifier.add p (Result.Res (normalized_guards,goal))
with exn ->
- Quantifier.add p (Err exn)
+ Quantifier.add p (Result.Err exn)
module Preprocessor : sig
val compute : file -> unit
@@ -687,11 +689,11 @@ end
| Pforall _ ->
Quantifier.add
p
- (Err (Error.Not_yet "unguarded \\forall quantification"))
+ (Result.Err (Error.make_not_yet "unguarded \\forall quantification"))
| Pexists _ ->
Quantifier.add
p
- (Err (Error.Not_yet "unguarded \\exists quantification"))
+ (Result.Err (Error.make_not_yet "unguarded \\exists quantification"))
| _ -> ()
let do_user_predicates () =
diff --git a/src/plugins/e-acsl/src/analyses/bound_variables.mli b/src/plugins/e-acsl/src/analyses/bound_variables.mli
index 688e5c1ac9ef90761576655d6169c2204fe8e018..e3bf6ea78ebe48e89823eda5d9e9548ffe69a0e6 100644
Binary files a/src/plugins/e-acsl/src/analyses/bound_variables.mli and b/src/plugins/e-acsl/src/analyses/bound_variables.mli differ
diff --git a/src/plugins/e-acsl/src/analyses/interval.ml b/src/plugins/e-acsl/src/analyses/interval.ml
index 42c19e2aeb1608d5a68bfc6db6dc259fd93a7ba8..65c0a28875efff46b9dd1967ad788b95ce3a8cbd 100644
--- a/src/plugins/e-acsl/src/analyses/interval.ml
+++ b/src/plugins/e-acsl/src/analyses/interval.ml
@@ -26,6 +26,8 @@ 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.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 dc76e43c7502f4b9620545f9108048f09939b646..304ced042c78f899d15921da7e6190e9b37e994a 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
+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! *)
Rtl.Symbols.mem_vi vi.vname
@@ -42,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 18ebf2bfe89ffd54989c2ec9ce42d36e10bc8600..bf14a866a21515dcb6b0ab59b90d2bdd7b55778c 100644
--- a/src/plugins/e-acsl/src/analyses/typing.ml
+++ b/src/plugins/e-acsl/src/analyses/typing.ml
@@ -25,7 +25,8 @@ open Cil_types
(* Implement Figure 4 of J. Signoles' JFLA'15 paper "Rester statique pour
devenir plus rapide, plus précis et plus mince". *)
-let dkey = Options.dkey_typing
+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
@@ -197,9 +198,9 @@ module Memo: sig
lenv:Function_params_ty.t ->
(term -> computed_info) ->
term ->
- computed_info Error.or_error
+ computed_info Result.t
val get: lenv:Function_params_ty.t -> term ->
- computed_info Error.or_error
+ computed_info Result.t
val clear: unit -> unit
end = struct
@@ -217,7 +218,7 @@ end = struct
the guard and once for encoding [x+1] when incrementing it. The
memoization is only useful here and indeed prevent the generation of one
extra variable in some cases. *)
- let tbl : computed_info Error.or_error Misc.Id_term.Hashtbl.t =
+ let tbl : computed_info Result.t Misc.Id_term.Hashtbl.t =
Misc.Id_term.Hashtbl.create 97
(* The type of the logic function
@@ -230,7 +231,7 @@ end = struct
We distinguish the calls to the function by storing the type of the
arguments corresponding to each call, and we weaken the typing so that it
is invariant when the arguments have the same type. *)
- let dep_tbl : computed_info Error.or_error Id_term_with_lenv.Hashtbl.t
+ let dep_tbl : computed_info Result.t Id_term_with_lenv.Hashtbl.t
= Id_term_with_lenv.Hashtbl.create 97
let get_dep lenv t =
@@ -250,8 +251,8 @@ end = struct
try Misc.Id_term.Hashtbl.find tbl t
with Not_found ->
let x =
- try Error.Res (f t)
- with Error.Not_yet _ | Error.Typing_error _ as exn -> Error.Err exn
+ try Result.Res (f t)
+ with Error.Not_yet _ | Error.Typing_error _ as exn -> Result.Err exn
in
Misc.Id_term.Hashtbl.add tbl t x;
x
@@ -261,8 +262,8 @@ end = struct
Id_term_with_lenv.Hashtbl.find dep_tbl (t, lenv)
with Not_found ->
let x =
- try Error.Res (f t)
- with Error.Not_yet _ | Error.Typing_error _ as exn -> Error.Err exn
+ try Result.Res (f t)
+ with Error.Not_yet _ | Error.Typing_error _ as exn -> Result.Err exn
in
Id_term_with_lenv.Hashtbl.add dep_tbl (t, lenv) x;
x
@@ -882,6 +883,7 @@ and type_predicate ~lenv p =
"preprocessing of quantified predicate"
Bound_variables.get_preprocessed_quantifier
p
+ Printer.pp_predicate
in
let guards =
List.map
@@ -938,9 +940,9 @@ let unsafe_set t ?ctx ~lenv ty =
(******************************************************************************)
let get_number_ty ~lenv t =
- (Error.retrieve_preprocessing "typing" (Memo.get ~lenv) t).ty
+ (Error.retrieve_preprocessing "typing" (Memo.get ~lenv) t Printer.pp_term).ty
let get_integer_op ~lenv t =
- (Error.retrieve_preprocessing "typing" (Memo.get ~lenv) t).op
+ (Error.retrieve_preprocessing "typing" (Memo.get ~lenv) t Printer.pp_term).op
let get_integer_op_of_predicate ~lenv p = (type_predicate ~lenv p).op
(* {!typ_of_integer}, but handle the not-integer cases. *)
@@ -956,15 +958,18 @@ let extract_typ t ty =
| Larrow _ -> Error.not_yet "unsupported logic type: type arrow"
let get_typ ~lenv t =
- let info = Error.retrieve_preprocessing "typing" (Memo.get ~lenv) t in
+ let info =
+ Error.retrieve_preprocessing "typing" (Memo.get ~lenv) t Printer.pp_term in
extract_typ t info.ty
let get_op ~lenv t =
- let info = Error.retrieve_preprocessing "typing" (Memo.get ~lenv) t in
+ let info =
+ Error.retrieve_preprocessing "typing" (Memo.get ~lenv) t Printer.pp_term in
extract_typ t info.op
let get_cast ~lenv t =
- let info = Error.retrieve_preprocessing "typing" (Memo.get ~lenv) t in
+ let info =
+ Error.retrieve_preprocessing "typing" (Memo.get ~lenv) t Printer.pp_term in
try Option.map typ_of_number_ty info.cast
with Not_a_number -> None
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..f7c37db6cc45850e644a7a895f827e7573721a18 100644
--- a/src/plugins/e-acsl/src/code_generator/injector.ml
+++ b/src/plugins/e-acsl/src/code_generator/injector.ml
@@ -23,8 +23,9 @@
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
+let dkey = Options.Dkey.translation
(* ************************************************************************** *)
(* Expressions *)
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/quantif.ml b/src/plugins/e-acsl/src/code_generator/quantif.ml
index 2a5e0a68adecde5556a6eee78f339655f409245d..ee06ec1a361e00a594d3074f20d374b0b81886d2 100644
--- a/src/plugins/e-acsl/src/code_generator/quantif.ml
+++ b/src/plugins/e-acsl/src/code_generator/quantif.ml
@@ -71,6 +71,7 @@ let convert kf env loc ~is_forall quantif =
"preprocessing of quantified predicate"
Bound_variables.get_preprocessed_quantifier
quantif
+ Printer.pp_predicate
in
match has_empty_quantif_with_false_negative bound_vars, is_forall with
| true, true ->
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_predicates.ml b/src/plugins/e-acsl/src/code_generator/translate_predicates.ml
index dd9bd7e229511cc17a94b83b5c99601c1b3218f3..ad2490808de071d5a3775c82dd9c53fac67f44ea 100644
--- a/src/plugins/e-acsl/src/code_generator/translate_predicates.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate_predicates.ml
@@ -24,7 +24,7 @@
open Cil_types
open Cil_datatype
-let dkey = Options.dkey_translation
+let dkey = Options.Dkey.translation
(**************************************************************************)
(********************** Forward references ********************************)
diff --git a/src/plugins/e-acsl/src/code_generator/translate_rtes.ml b/src/plugins/e-acsl/src/code_generator/translate_rtes.ml
index 5aca164b247a1383f89861087862011eb670aab2..cb3175ec9401dc17fdb59362a8aab257cea1f646 100644
--- a/src/plugins/e-acsl/src/code_generator/translate_rtes.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate_rtes.ml
@@ -23,7 +23,7 @@
(** Generate and translate RTE annotations. *)
open Cil_types
-let dkey = Options.dkey_translation
+let dkey = Options.Dkey.translation
let rte_annots pp elt kf env l =
let old_kind = Env.annotation_kind env in
diff --git a/src/plugins/e-acsl/src/code_generator/translate_terms.ml b/src/plugins/e-acsl/src/code_generator/translate_terms.ml
index 7506c183009b3c3dd5ee33141d4d3887fc686741..855400bbda51f71080f98de7caa86f88225575cb 100644
--- a/src/plugins/e-acsl/src/code_generator/translate_terms.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate_terms.ml
@@ -23,7 +23,7 @@
(** Generate C implementations of E-ACSL terms. *)
open Cil_types
-let dkey = Options.dkey_translation
+let dkey = Options.Dkey.translation
(**************************************************************************)
(********************** Forward references ********************************)
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..5636d7d244c6781e810aedc9dfeeafefaa53e3d1
--- /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
diff --git a/src/plugins/e-acsl/src/libraries/error.ml b/src/plugins/e-acsl/src/libraries/error.ml
index 6062ebdf0d6976ed1537f90c9d10dbda579798cd..98e9ecefb42709dd98cb1da72ffc78f41610ad70 100644
--- a/src/plugins/e-acsl/src/libraries/error.ml
+++ b/src/plugins/e-acsl/src/libraries/error.ml
@@ -20,72 +20,105 @@
(* *)
(**************************************************************************)
-exception Ignored
-let ignored () = raise Ignored
+(** Internal module holding the exception of [Error].
-exception Typing_error of string
-let untypable s = raise (Typing_error s)
+ The module is included into [Make_with_opt] later and should not be used
+ directly. However we need to have a separate module for the exception so
+ that every exception built by [Make] is the exact same type. *)
+module Exn = struct
+ exception Typing_error of Options.category option * string
+ exception Not_yet of Options.category option * string
+ exception Not_memoized of Options.category option
+end
-exception Not_yet of string
-let not_yet s = raise (Not_yet s)
+module type S = sig
+ include module type of Exn
+ val make_untypable: string -> exn
+ val make_not_yet: string -> exn
+ val make_not_memoized: unit -> exn
+ val untypable: string -> 'a
+ val not_yet: string -> 'a
+ val not_memoized: unit -> 'a
+ val print_not_yet: string -> unit
+ val handle: ('a -> 'a) -> 'a -> 'a
+ val generic_handle: ('a -> 'b) -> 'b -> 'a -> 'b
+ val retrieve_preprocessing:
+ string ->
+ ('a -> 'b Result.t) ->
+ 'a ->
+ (Format.formatter -> 'a -> unit) ->
+ 'b
+end
-exception Not_memoized
-let not_memoized () = raise Not_memoized
+module Make_with_opt(P: sig val phase:Options.category option end): S = struct
+ include Exn
-module Nb_typing =
- State_builder.Ref
- (Datatype.Int)
- (struct
- let name = "E_ACSL.Error.Nb_typing"
- let default () = 0
- let dependencies = [ Ast.self ]
- end)
+ let make_untypable msg = Typing_error (P.phase, msg)
+ let make_not_yet msg = Not_yet (P.phase, msg)
+ let make_not_memoized () = Not_memoized P.phase
-let nb_untypable = Nb_typing.get
+ let untypable msg = raise (make_untypable msg)
+ let not_yet msg = raise (make_not_yet msg)
+ let not_memoized () = raise (make_not_memoized ())
-module Nb_not_yet =
- State_builder.Ref
- (Datatype.Int)
- (struct
- let name = "E_ACSL.Error.Nb_not_yet"
- let default () = 0
- let dependencies = [ Ast.self ]
- end)
+ let pp_phase fmt phase =
+ match phase with
+ | Some phase ->
+ if Options.verbose_atleast 2 then
+ Format.fprintf fmt "@[@ in phase `%a'@]" Options.pp_category phase
+ | None -> ()
-let nb_not_yet = Nb_not_yet.get
+ let do_print_not_yet phase msg =
+ let msg =
+ Format.asprintf
+ "@[E-ACSL construct@ `%s'@ is not yet supported%a.@]"
+ msg
+ pp_phase phase
+ in
+ Options.warning
+ ~once:true ~current:true
+ "@[%s@ Ignoring annotation.@]" msg
-let print_not_yet msg =
- let msg =
- Format.sprintf "@[E-ACSL construct@ `%s'@ is not yet supported.@]" msg
- in
- Options.warning ~once:true ~current:true "@[%s@ Ignoring annotation.@]" msg;
- Nb_not_yet.set (Nb_not_yet.get () + 1)
+ let print_not_yet msg =
+ do_print_not_yet P.phase msg
-let generic_handle f res x =
- try
- f x
- with
- | Typing_error s ->
- let msg = Format.sprintf "@[invalid E-ACSL construct@ `%s'.@]" s in
- Options.warning ~once:true ~current:true "@[%s@ Ignoring annotation.@]" msg;
- Nb_typing.set (Nb_typing.get () + 1);
- res
- | Not_yet s ->
- print_not_yet s;
- res
- | Ignored -> res
+ let generic_handle f res x =
+ try
+ f x
+ with
+ | Typing_error (phase, s) ->
+ let msg =
+ Format.asprintf "@[invalid E-ACSL construct@ `%s'%a.@]"
+ s
+ pp_phase phase
+ in
+ Options.warning
+ ~once:true ~current:true
+ "@[%s@ Ignoring annotation.@]" msg;
+ res
+ | Not_yet (phase, s) ->
+ do_print_not_yet phase s;
+ res
-let handle f x = generic_handle f x x
+ let handle f x = generic_handle f x x
-type 'a or_error = Res of 'a | Err of exn
+ let retrieve_preprocessing analyse_name getter parameter pp =
+ try
+ match getter parameter with
+ | Result.Res res -> res
+ | Result.Err exn -> raise exn
+ with Not_memoized phase ->
+ Options.fatal
+ "@[%s was not performed on construct %a%a@]"
+ analyse_name
+ pp parameter
+ pp_phase phase
+end
-let retrieve_preprocessing analyse_name getter parameter =
- try
- match getter parameter with
- | Res res -> res
- | Err exn -> raise exn
- with Not_memoized ->
- Options.fatal "%s was not performed on construct" analyse_name
+module Make(P: sig val phase:Options.category end): S =
+ Make_with_opt(struct let phase = Some P.phase end)
+
+include Make_with_opt(struct let phase = None end)
(*
Local Variables:
diff --git a/src/plugins/e-acsl/src/libraries/error.mli b/src/plugins/e-acsl/src/libraries/error.mli
index 9dcc0355b6138e532e11a285244655646958be28..b36dd277dcfd93e3a7e86827356b7fc46cd740c3 100644
--- a/src/plugins/e-acsl/src/libraries/error.mli
+++ b/src/plugins/e-acsl/src/libraries/error.mli
@@ -22,50 +22,66 @@
(** Handling errors. *)
-exception Ignored
-exception Typing_error of string
-exception Not_yet of string
-exception Not_memoized
+module type S = sig
+ exception Typing_error of Options.category option * string
+ (** Typing error where the first element is the phase where the error occured
+ and the second element is the error message. *)
-type 'a or_error = Res of 'a | Err of exn
+ exception Not_yet of Options.category option * string
+ (** "Not yet supported" error where the first element is the phase where the
+ error occured and the second element is the error message. *)
-val untypable: string -> 'a
-(** Type error built from the given argument. *)
+ exception Not_memoized of Options.category option
+ (** "Not memoized" error with the phase where the error occured. *)
-val not_yet: string -> 'a
-(** Not_yet_implemented error built from the given argument. *)
+ val make_untypable: string -> exn
+ (** Make a [Typing_error] exception with the given message. *)
-val ignored: unit -> 'a
-(** Statement already signaled and marked as ignored *)
+ val make_not_yet: string -> exn
+ (** Make a [Not_yet] exception with the given message. *)
-val not_memoized : unit -> 'a
-(** @raise Not_memoized when asking the preprocessed form of something that
- was not preprocessed *)
+ val make_not_memoized: unit -> exn
+ (** Make a [Not_memoized] exception with the given message. *)
-val handle: ('a -> 'a) -> 'a -> 'a
-(** Run the closure with the given argument and handle potential errors.
- Return the provide argument in case of errors. *)
+ val untypable: string -> 'a
+ (** @raise Typing_error with the given message for the current phase. *)
-val generic_handle: ('a -> 'b) -> 'b -> 'a -> 'b
-(** Run the closure with the given argument and handle potential errors.
- Return the additional argument in case of errors. *)
+ val not_yet: string -> 'a
+ (** @raise Not_yet with the given message for the current phase. *)
-val nb_untypable: unit -> int
-(** Number of untypable annotations. *)
+ val not_memoized: unit -> 'a
+ (** @raise Not_memoized for the current phase. *)
-val nb_not_yet: unit -> int
-(** Number of not-yet-supported annotations. *)
+ val print_not_yet: string -> unit
+ (** Print the "not yet supported" message without raising an exception. *)
-val print_not_yet: string -> unit
-(** Print the "not yet" message without raising an exception. *)
+ val handle: ('a -> 'a) -> 'a -> 'a
+ (** Run the closure with the given argument and handle potential errors.
+ Return the provide argument in case of errors. *)
-val retrieve_preprocessing: string -> ('a -> 'b or_error) -> 'a -> 'b
-(** Retrieve the result of a preprocessing phase, which possibly failed.
- The [string] argument is used to display a message in case the preprocessing
- phase did not compute the required result. *)
+ val generic_handle: ('a -> 'b) -> 'b -> 'a -> 'b
+ (** Run the closure with the given argument and handle potential errors.
+ Return the additional argument in case of errors. *)
+
+ val retrieve_preprocessing:
+ string ->
+ ('a -> 'b Result.t) ->
+ 'a ->
+ (Format.formatter -> 'a -> unit) ->
+ 'b
+ (** Retrieve the result of a preprocessing phase, which possibly failed.
+ The [string] argument and the formatter are used to display a message in
+ case the preprocessing phase did not compute the required result. *)
+end
+
+(** Functor to build an [Error] module for a given [phase]. *)
+module Make(P: sig val phase:Options.category end): S
+
+(** The [Error] module implements [Error.S] with no phase. *)
+include S
(*
Local Variables:
-compile-command: "make"
+compile-command: "make -C ../../../../.."
End:
*)
diff --git a/src/plugins/e-acsl/src/libraries/result.ml b/src/plugins/e-acsl/src/libraries/result.ml
new file mode 100644
index 0000000000000000000000000000000000000000..701b5dd6d6fae32831a676d4f35f29bad9e1a83e
--- /dev/null
+++ b/src/plugins/e-acsl/src/libraries/result.ml
@@ -0,0 +1,30 @@
+(**************************************************************************)
+(* *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+(** Type holding a result or an exception *)
+
+type 'a t = Res of 'a | Err of exn
+
+let pretty pp fmt result =
+ match result with
+ | Res a -> Format.fprintf fmt "@[%a@]" pp a
+ | Err err -> Format.fprintf fmt "@[%s@]" (Printexc.to_string err)
diff --git a/src/plugins/e-acsl/src/libraries/result.mli b/src/plugins/e-acsl/src/libraries/result.mli
new file mode 100644
index 0000000000000000000000000000000000000000..d992f305fc630253a6bb6117a2318a4e9ae2f712
--- /dev/null
+++ b/src/plugins/e-acsl/src/libraries/result.mli
@@ -0,0 +1,34 @@
+(**************************************************************************)
+(* *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+(** Type holding a result or an exception *)
+
+(** Represent either a result of type ['a] or an error with an exception *)
+type 'a t = Res of 'a | Err of exn
+
+val pretty:
+ (Format.formatter -> 'a -> unit) ->
+ Format.formatter ->
+ 'a t ->
+ unit
+(** [pretty pp] where [pp] is a formatter for ['a] returns a formatter for
+ ['a t]. *)
diff --git a/src/plugins/e-acsl/src/options.ml b/src/plugins/e-acsl/src/options.ml
index 3aa05ca87e7c9a344e71eaad8dfcb5ca1759cfd1..900473331b65e47b4d8c3a6ef474719aee98dd23 100644
--- a/src/plugins/e-acsl/src/options.ml
+++ b/src/plugins/e-acsl/src/options.ml
@@ -172,10 +172,14 @@ let emitter =
let must_visit () = Run.get ()
-let dkey_analysis = register_category "analysis"
-let dkey_prepare = register_category "preparation"
-let dkey_translation = register_category "translation"
-let dkey_typing = register_category "typing"
+module Dkey = struct
+ let prepare = register_category "preparation"
+ let bound_variables = register_category "analysis:bound_variables"
+ let interval = register_category "analysis:interval_inference"
+ let mtracking = register_category "analysis:memory_tracking"
+ let typing = register_category "analysis:typing"
+ let translation = register_category "translation"
+end
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..b0a91ccbc3b369032048f946c030ca55e05fa8af 100644
--- a/src/plugins/e-acsl/src/options.mli
+++ b/src/plugins/e-acsl/src/options.mli
@@ -41,10 +41,14 @@ val emitter: Emitter.t
val must_visit: unit -> bool
-val dkey_analysis: category
-val dkey_prepare: category
-val dkey_translation: category
-val dkey_typing: category
+module Dkey: sig
+ val prepare: category
+ val bound_variables: category
+ val interval: category
+ val mtracking: category
+ val typing: category
+ val translation: category
+end
val setup: ?rtl:bool -> unit -> unit
(** Verify and initialize the options of the current project according to the
diff --git a/src/plugins/e-acsl/src/project_initializer/prepare_ast.ml b/src/plugins/e-acsl/src/project_initializer/prepare_ast.ml
index ff197b64c36ce46d2ffb60df5b229cf121d27bb4..fba831fb6b7465813c13ae41d6729039444ca8e8 100644
--- a/src/plugins/e-acsl/src/project_initializer/prepare_ast.ml
+++ b/src/plugins/e-acsl/src/project_initializer/prepare_ast.ml
@@ -23,7 +23,7 @@
open Cil_types
open Cil_datatype
-let dkey = Options.dkey_prepare
+let dkey = Options.Dkey.prepare
(**************************************************************************)
(********************** Forward references ********************************)