goblint
Support for `atexit`, `on_exit` and `pthread_cleanup_*` handlers
Those are features we currently do not support yet, but it might be interesting to do so.
While looking at Concrat again, I found out that pthread_cleanup_push is a macro which doesn't actually store the cleanup routine is some magic place, but implements it using some flavor of setjmp. It's just that the longjmp isn't explicit, rather but that's what pthread does magically with __pthread_register_cancel.
Perhaps it's possible to handle __pthread_register_cancel specially as triggering a longjmp and unwinding the stack. Actually the longjmp can happen anywhere in a nested function call, but maybe that doesn't really matter? What's important is that there is something which unwinds the stack back.
I learned today that GCC/Clang also have a __cleanup__ attribute which gives C++ RAII-like features in C. And it's starting to be used in the Linux kernel: https://lwn.net/Articles/934679/.
It's more fine-grained than the functions listed in the issue (and requires block scope support!), but might become relevant if we try to analyze the modern kernel. Not handling them could easily make us very unsound: we just ignore the attribute and perhaps never consider some mutexes unlocked.