It seems that pthread_mutex_t is an opaque pointer (you could track the typedef down to find out). In Splint, pointers are not-nullable by default. If you want to have a nullable pointer, you must declare it with the semantic annotation /*@null@*/, for example:
char * ptr1;
/*@null@*/ char * ptr2;
ptr1 = NULL; /* warning: implicitly not-nullable pointer */
ptr2 = NULL; /* OK: explicitly nullable pointer */
According to the manual, there are 3 options regarding null state:
null Possibly null pointer.notnull Non-null pointer.relnull Relax null checking. No errors when NULL is assigned to it, or when it is used as a non-null pointer.
The advantage of using not-nullable pointers is that you don t need to check them every time you get one of them. For example, you could annotate a function parameter as /*@notnull@*/ and then you are not required to check if(pointer == NULL) before you dereference it. This reduces checking and simplifies your code.
The danger of ignoring these warnings is that, if you are telling Splint that a specific pointer can t possibly be null and later on you try to assign NULL to it, this null pointer could end up being derefered and the program could crash.
In my opinion, your actual issue is Splint s policy, which considers all pointers implicitly not-nullable. This forces you to annotate all your possibly null pointers.
