Dynamically linking with Why3 should not change the signal handlers
We found out that dynamically linking Why3 was messing up the sigint
handling (with Sys.catch_break true
, catching Sys.Break
) in our code. Why3 changes the signal handler during load in debug.ml.
We are relying on the exception mechanism to ensure that the deallocation process always holds (catch - deallocate - reraise) and to exits gracefully on user Ctrl+C
. The first problem is more annoying with some libraries (e.g. zmq
) where not deallocating properly leads to a frozen process after Ctrl+C
that can only be killed with other signals.
I think that dynamically loading a library should not change the handlers that have already been set by the main process.