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.