From 374b2467bc0ef421aa22a249922205de6d0e937a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Fri, 9 Oct 2020 19:09:44 +0200
Subject: [PATCH] [wp] protected exceptions
---
src/plugins/wp/wp_parameters.ml | 10 ++++++++++
src/plugins/wp/wp_parameters.mli | 2 ++
2 files changed, 12 insertions(+)
diff --git a/src/plugins/wp/wp_parameters.ml b/src/plugins/wp/wp_parameters.ml
index 94f5b8131ff..9335161d010 100644
--- a/src/plugins/wp/wp_parameters.ml
+++ b/src/plugins/wp/wp_parameters.ml
@@ -1239,3 +1239,13 @@ let print_generated ?header file =
end
(* -------------------------------------------------------------------------- *)
+(* --- Debugging --- *)
+(* -------------------------------------------------------------------------- *)
+
+let protect e =
+ if debug_atleast 1 then false else
+ match e with
+ | Db.Cancel | Log.AbortError _ | Log.AbortFatal _ -> false
+ | _ -> true
+
+(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/wp_parameters.mli b/src/plugins/wp/wp_parameters.mli
index a37b5e895a7..97392faa580 100644
--- a/src/plugins/wp/wp_parameters.mli
+++ b/src/plugins/wp/wp_parameters.mli
@@ -175,3 +175,5 @@ val print_generated: ?header:string -> string -> unit
(** print the given file if the debugging category
"print-generated" is set *)
val cat_print_generated: category
+
+val protect : exn -> bool
--
GitLab