From f374b79e08e135de11def93005110a833686c5f7 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Mon, 1 Apr 2019 17:41:22 +0200 Subject: Protect some I/O routines from SIGALRM This is necessary to prevent Coq from sending ill-formed output in some scenarios involving `Timeout`. Co-authored-by: Enrico Tassi --- lib/control.ml | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) (limited to 'lib/control.ml') diff --git a/lib/control.ml b/lib/control.ml index ffb3584f1e..9054507e46 100644 --- a/lib/control.ml +++ b/lib/control.ml @@ -89,3 +89,21 @@ let timeout_fun_ref = ref timeout_fun let set_timeout f = timeout_fun_ref := f let timeout n f e = !timeout_fun_ref.timeout n f e + +let protect_sigalrm f x = + let timed_out = ref false in + let timeout_handler _ = timed_out := true in + try + let old_handler = Sys.signal Sys.sigalrm (Sys.Signal_handle timeout_handler) in + try + let res = f x in + Sys.set_signal Sys.sigalrm old_handler; + match !timed_out, old_handler with + | true, Sys.Signal_handle f -> f Sys.sigalrm; res + | _, _ -> res + with e -> + let e = Backtrace.add_backtrace e in + Sys.set_signal Sys.sigalrm old_handler; + Exninfo.iraise e + with Invalid_argument _ -> (* This happens on Windows, as handling SIGALRM does not seem supported *) + f x -- cgit v1.2.3