Null Dereferences

A common cause of program failures is when a null pointer is dereferenced.
Splint detects these errors by distinguishing possibly NULL pointers at interface boundaries.
The null annotation is used to indicate that a pointer value may be NULL.
A pointer declared with no null annotation, may not be NULL.
If null checking is turned on (controlled by null), Splint will report an error when a possibly null pointer is passed as a parameter, returned as a result, or assigned to an external reference with no null qualifier.
If a pointer is declared with the null annotation, the code must check that it is not NULL on all paths leading to a dereference of the pointer (or the pointer being returned or passed as a value with no null annotation).
Dereferences of possibly null pointers may be protected by conditional statements or assertions (to see how assert is declared see Section 8.1) that check the pointer is not NULL.
Consider two implementations of firstChar in Figure 2.
For firstChar1, Splint reports an error since the pointer that is dereferenced is declared with a null annotation.
For firstChar2, no error is reported since the true branch of the s == NULL if statement returns, so the dereference of s is only reached if s is not NULL.

Predicate Functions

Notnull Annotations

Relaxing Null Checking

最終更新:2008年12月16日 20:31