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.
|
null.c |
Running Splint |
|
char firstChar1 (/*@null@*/ char *s) { }
char firstChar2 (/*@null@*/ char *s) { if
(s == NULL) return ‘\0’; } |
> splint null.c Splint 3.0.1
null.c: (in function firstChar1) null.c:3:11: Dereference of possibly null pointer s: *s null.c:1:35: Storage s may become null
Finished checking --- 1 code warning found
|
|
Figure 2. Null Checking Output from running Splint is displayed in sans-serif font. The command line is preceded by >, the rest is output from Splint. Explanations added to the code or splint output are shown in italics. Code shown in the figures in this document is available from the splint web site, http://www.splint.org . No error is reported for line 9, since the dereference is reached only if s is non-null. For most of the figures, the options -linelen 55 -hints –showcol were used to produce condensed output, and –exportlocal to inhibit warnings about exported declarations. |
Another way to protect null dereference, is to declare a function using nullwhentrue or falsewhennull(these annotations where originally falsenull and truenull, but were renamed to clarify the logical asymmetry; falsenull and truenull may still be used) and call the function in a conditional statement before the null-annotated pointer is dereferenced.
If a function annotated with nullwhentrue returns true it means its first passed parameter is NULL. If it returns false, the parameter is not NULL. Note that it may return true for a parameter that is not NULL. A more descriptive name for nullwhentrue would be “if the result is false, the parameter was not null”. For example, if isNull is declared as,
/*@nullwhentrue@*/ bool isNull (/*@null@*/ char *x);
we could write firstChar2:
char firstChar2 (/*@null@*/ char *s)
{
if (isNull (s)) return
'\0';
return *s;
}
No error is reported since the dereference of s is only reached if isNull(s) is false, and since isNull is declared with the nullwhentrue annotation this means s must not be null.
The falsewhennull annotation is not quite the logical opposite of nullwhentrue. If a function declared with falsewhennull returns true, it means its parameter is definitely not NULL. If it returns false, the parameter may or may not be NULL. That is a falsewhennull always returns false when passed a NULL parameter; it may sometimes return false when passed a non-NULL parameter.
For example, we could define isNonEmpty to return true if its parameter is not NULL and has least one character before the NUL terminator:
/*@falsewhennull@*/ bool isNonEmpty (/*@null@*/ char *x)
{
return (x != NULL && *x != ‘\0’);
}
Splint does not check that the implementation of a function declared with nullwhentrue or falsewhennull is consistent with its annotation, but assumes the annotation is correct when code that calls the function is checked.
The notnull annotation specifies that a declarator is definitely not NULL. By default, this is assumed, but it may be necessary to use notnull to override a null in a type definition. The null annotation may be used in a type definition to indicate that all instances of the type may be NULL. For declarations of a type declared using null, the null annotation in the type definition may be overridden with notnull. This is particularly useful for parameters to hidden static operations of abstract types (see Section 4.3) where the null test has already been done before the function is called, or function results known to never be NULL. For an abstract type, notnull may not be used for parameters to external functions, since clients should not be aware of when the concrete representation may by NULL. Parameters to static functions in the implementation module, however, may be declared using notnull, since they may only be called from places where the representation is accessible. Return values for static or external functions may be declared using notnull.
An additional annotation, relnull may be used to relax null checking. No error is reported when a relnull value is dereferenced, or when a possibly null value is assigned to an identifier declared using relnull.
This is generally used for structure fields that may or may not be null depending on some other constraint. Splint does not report and error when NULL is assigned to a relnull reference, or when a relnull reference is dereferenced. It is up to the programmer to ensure that this constraint is satisfied before the pointer is dereferenced.
Next: 3. Undefined Values
Return to Contents