Fix #13739 - disable some warnings when calling Function.

Also added a generic way of temporarily disabling a warning.
Also added try_finalize un lib/utils.ml.

4 files changed, 29 insertions, 0 deletions

diff --git a/lib/cWarnings.ml b/lib/cWarnings.ml
index cc1fa647f9..ee7dab92bc 100644
--- a/lib/cWarnings.ml
+++ b/lib/cWarnings.ml
@@ -173,3 +173,9 @@ let create ~name ~category ?(default=Enabled) pp =
     | Disabled -> ()
     | AsError -> CErrors.user_err ?loc (pp x)
     | Enabled -> Feedback.msg_warning ?loc (pp x)
+
+(* Remark: [warn] does not need to start with a comma, but if present
+   it won't hurt (",," is normalized into ","). *)
+let with_warn warn (f:'b -> 'a) x =
+  let s = get_flags () in
+  Util.try_finally (fun x -> set_flags (s^","^warn);f x) x set_flags s
diff --git a/lib/cWarnings.mli b/lib/cWarnings.mli
index ded1f9be3b..b63eed09d0 100644
--- a/lib/cWarnings.mli
+++ b/lib/cWarnings.mli
@@ -19,3 +19,10 @@ val set_flags : string -> unit
 (** Cleans up a user provided warnings status string, e.g. removing unknown
     warnings (in which case a warning is emitted) or subsumed warnings . *)
 val normalize_flags_string : string -> string
+
+(** [with_warn "-xxx,+yyy..." f x] calls [f x] after setting the
+   warnings as specified in the string (keeping other previously set
+   warnings), and restores current warnings after [f()] returns or
+   raises an exception. If both f and restoring the warnings raise
+   exceptions, the latter is raised. *)
+val with_warn: string -> ('b -> 'a) -> 'b -> 'a
diff --git a/lib/util.ml b/lib/util.ml
index 87cc30e557..e8aa0f3e48 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -135,6 +135,13 @@ type 'a delayed = unit -> 'a
 
 let delayed_force f = f ()
 
+(* finalize - Credit X.Leroy, D.Remy. *)
+let try_finally f x finally y =
+  let res = try f x with exn -> finally y; raise exn in
+  finally y;
+  res
+
+
 (* Misc *)
 
 type ('a, 'b) union = ('a, 'b) CSig.union = Inl of 'a | Inr of 'b
diff --git a/lib/util.mli b/lib/util.mli
index fe34525671..aefb015c38 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -112,6 +112,15 @@ type 'a delayed = unit -> 'a
 
 val delayed_force : 'a delayed -> 'a
 
+(** [try_finally f x g y] applies the main code [f] to [x] and
+   returns the result after having applied the finalization
+   code [g] to [y]. If the main code raises the exception
+   [exn], the finalization code is executed and [exn] is raised.
+   If the finalization code itself fails, the exception
+   returned is always the one from the finalization code.
+   Credit X.Leroy, D.Remy. *)
+val try_finally: ('a -> 'b) -> 'a -> ('c -> unit) -> 'c -> 'b
+
 (** {6 Enriched exceptions} *)
 
 type iexn = Exninfo.iexn