For the RefPerSys project (Linux/x86-64, GPLv3+ licensed), its refpersys-in-c variant, commit 1441e0fa148d, I am seeking a source code analyzer which checks that calls to
pthread_mutex_unlock are well balanced.
I am aware that in general the question is undecidable (Rice's theorem).
For refpersys-in-c the C code should be "simple enough" to be probably analyzable in practice by simple automatic tools. We tried hard to avoid complex control flows.
pthread_mutex_t are either global or static, or inside the
RpsObject_t type (defined in header