Goblint makes the following (implicit) assumptions about the systems and programs it analyzes.

NB! This list is likely incomplete.

  1. PTHREAD_MUTEX_DEFAULT is a non-recursive mutex type.

    Although the POSIX Programmer's Manual states that

    An implementation may map this mutex to one of the other mutex types.

    including PTHREAD_MUTEX_RECURSIVE, on Linux and OSX it seems to be mapped to PTHREAD_MUTEX_NORMAL. Goblint assumes this to be the case.

    This affects the maylocks analysis.

    See PR #1414.