From 3275ea5164fab7460807afda4eb97d58ba0a768a Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Tue, 22 Sep 2020 09:58:38 +0200
Subject: [PATCH] [eacsl:libs] Extract the processing of annotation errors in a
separate function
---
src/plugins/e-acsl/src/libraries/error.ml | 21 ++++++++++++++-------
src/plugins/e-acsl/src/libraries/error.mli | 7 +++++++
2 files changed, 21 insertions(+), 7 deletions(-)
diff --git a/src/plugins/e-acsl/src/libraries/error.ml b/src/plugins/e-acsl/src/libraries/error.ml
index a572ecdffc6..5c8fec2f96b 100644
--- a/src/plugins/e-acsl/src/libraries/error.ml
+++ b/src/plugins/e-acsl/src/libraries/error.ml
@@ -48,21 +48,28 @@ module Nb_not_yet =
let nb_not_yet = Nb_not_yet.get
-let generic_handle f res x =
- try
- f x
- with
+let process_error = function
| 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
+ Nb_typing.set (Nb_typing.get () + 1)
| Not_yet s ->
let msg =
Format.sprintf "@[E-ACSL construct@ `%s'@ is not yet supported.@]" s
in
Options.warning ~once:true ~current:true "@[%s@ Ignoring annotation.@]" msg;
- Nb_not_yet.set (Nb_not_yet.get () + 1);
+ Nb_not_yet.set (Nb_not_yet.get () + 1)
+ | exn ->
+ Options.fatal
+ "Unexpected error in `Error.process_error`: %s"
+ (Printexc.to_string exn)
+
+let generic_handle f res x =
+ try
+ f x
+ with
+ | exn ->
+ process_error exn;
res
let handle f x = generic_handle f x x
diff --git a/src/plugins/e-acsl/src/libraries/error.mli b/src/plugins/e-acsl/src/libraries/error.mli
index 34176dd34e9..2cbea96413a 100644
--- a/src/plugins/e-acsl/src/libraries/error.mli
+++ b/src/plugins/e-acsl/src/libraries/error.mli
@@ -45,6 +45,13 @@ val nb_untypable: unit -> int
val nb_not_yet: unit -> int
(** Number of not-yet-supported annotations. *)
+val process_error: exn -> unit
+(** Process the given error.
+
+ Print a warning message and update the number of not-yet-supported and
+ untypable annotations. Print a fatal message and abort in case of unknown
+ errors. *)
+
(*
Local Variables:
compile-command: "make"
--
GitLab