diff --git a/src/plugins/e-acsl/src/libraries/error.ml b/src/plugins/e-acsl/src/libraries/error.ml
index a572ecdffc6a5fe67deeb48d7c080553f05e6174..5c8fec2f96bad497e2fc39ac54922c8cdae233e0 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 34176dd34e93c7aebf4b0b244560fb0954c2ab98..2cbea96413ad43be6c127fb78694d697b6c86a7c 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"