uses a local variable before it is defined, a use before definition error is reported. Use before definition checking is controlled by the usedef flag.
LCLint can do more checking than standard checkers though, because the
annotations can be used to describe what storage must be defined and what
storage may be undefined at interface points. Unannotated references are
expected to be completely defined at interface points. This means all storage
reachable from a global variable, parameter to a function, or function return
value is defined before and after a function call.
7.1.1 Undefined Parameters
Sometimes, function parameters or return values are expected to reference
undefined or partially defined storage. For example, a pointer parameter may
be intended only as an address to store a result, or a memory allocator may
return allocated but undefined storage. The out annotation denotes a pointer
to storage that may be undefined.
LCLint does not report an error when a pointer to allocated but undefined storage is passed as an out parameter. Within the body of a function, LCLint will assume an out parameter is allocated but not necessarily bound to a value, so an error is reported if its value is used before it is defined.
LCLint reports an error if storage reachable by the caller after the call is not defined when the function returns. This can be suppressed by -mustdefine. When checking a call, an actual parameter corresponding to an out parameter is assumed to be completely defined after the call returns.
When checking unannotated programs, many spurious use before definition errors
may be reported If impouts is on, no error is reported when an
incompletely-defined parameter is passed to a formal parameter with no
definition annotation, and the actual parameter is assumed to be defined after
the call. The /*@in@*/ annotation can be used to denote a parameter that must
be completely defined, even if impouts is on. If impouts is off, there is an
implicit in annotation on every parameter with no definition annotation.
Figure 13. Use before definition.
7.1.2 Relaxing Checking
The reldef annotation relaxes definition checking for a particular declaration.
Storage declared with a reldef annotation is assumed to be defined when it is
used, but no error is reported if it is not defined before it is returned or
passed as a parameter.
It is up to the programmer to check reldef fields are used correctly. They
should be avoided in most cases, but may be useful for fields of structures
that may or may not be defined depending on other constraints.
7.1.3 Partially Defined Structures
The partial annotated can be used to relax checking of structure fields. A
structure with undefined fields may be passed as a partial parameter or
returned as a partial result. Inside a function body, no error is reported
when the field of a partial structure is used. After a call, all fields of a
structure that is passed as a partial parameter are assumed to be completely
defined.
7.1.4 Global Variables
Special annotations can be used in the globals list of a function declaration
(Section 4.2) to describe the states of global variables before and after the
call.
If a global is preceded by undef, it is assumed to be undefined before the call. Thus, no error is reported if the global is not defined when the function is called, but an error is reported if the global is used in the function body before it is defined.
The killed annotation denotes a global variable that may be undefined when the call returns. For globals that contain dynamically allocated storage, a killed global variable is similar to an only parameter (Section 5.2). An error is reported if it contains the only reference to storage that is not released before the call returns.
Figure 14. Annotated globals lists.
7.2 Null Pointers
A common cause of program failures is when a null pointer is dereferenced.
LCLint 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), LCLint 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 the 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 7.3) that check the pointer is not NULL.
Consider two implementations of firstChar in Figure 15. For firstChar1, LCLint 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.
A function is annotated with truenull is assumed to return TRUE if its first parameter is NULL and FALSE otherwise. For example, if isNull is declared as,
/*@truenull@*/ 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 truenull annotation this means s
must not be null.
The falsenull annotation is not quite the opposite of truenull. If a function declared with falsenull returns TRUE, it means its parameter is not NULL. If it returns FALSE, the parameter may or may not be NULL.
For example, we could define isNonEmpty to return TRUE if its parameter is not NULL and has least one character before the NUL terminator:
/*@falsenull@*/ bool isNonEmpty (/*@null@*/ char *x)
{
return (x != NULL && *x != `\0');
}
LCLint does not check that the implementation of a function declared with
falsenull or truenull is consistent with its annotation, but assumes the
annotation is correct when code that calls the function is checked.
7.2.3 Relaxing Null Checking
An additional annotation, relnull may be used to relax null checking (relnull
is analogous to reldef for definition 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. LCLint 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.
7.3 Execution
To detect certain errors and avoid spurious errors, it is important to know
something about the control flow behavior of called functions. Without
additional information, LCLint assumes that all functions eventually return and
execution continues normally at the call site.
The exits annotation is used to denote a function that never returns. For example,
extern /*@exits@*/ void fatalerror (/*@observer@*/ char *s);declares fatalerror to never return. This allows LCLint to correctly analyze code like,
if (x == NULL) fatalerror ("Yikes!");
*x = 3;
Other functions may exit, but sometimes (or usually) return normally. The
mayexit annotation denotes a function that may or may not return. This doesn't
help checking much, since LCLint must assume that a function declared with
mayexit returns normally when checking the code.
To be more precise, the trueexit and falseexit annotations may be used Similar to truenull and falsenull (see Section 7.2.1), trueexit and falseexit mean that a function always exits if the value of its first argument is TRUE or FALSE respectively. They may be used only on functions whose first argument has a boolean type.
A function declared with trueexit must exit if the value of its argument is TRUE, and a function declared with falseexit must exit if the value of its argument is FALSE. For example, the standard library declares assert as[20]:
/*@falseexit@*/ void assert (/*@sef@*/ bool /*@alt int@*/ pred);This way, code like,
assert (x != NULL);is checked correctly, since the falseexit annotation on assert means the deference of x is not reached is x != NULL is false.*x = 3;
Special clauses may be used to constrain the state of a parameter or return value before or after a call. One or more special clauses may appear in a function declaration, before the modifies or globals clauses. Special clauses may be listed in any order, but the same special clause should not be used more than once. Parameters used in special clauses must be annotated with /*@special@*/ in the function header. In a special clause list, result is used to refer to the return value of the function. If result appears in a special clause, the function return value must be annotated with /*@special@*/.
The following special clauses are used to describe the definition state or parameters before and after the function is called and the return value after the function returns:
/*@uses references@*/
References in the uses clause must be completely defined before the function is called. They are assumed to be defined at function entrance when the function is checked./*@sets references@*/
References in the sets clause must be allocated before the function is called. They are completely defined after the function returns. When the function is checked, they are assumed to be allocated at function entrance and an error is reported if there is a path on which they are not defined before the function returns./*@defines references@*/
References in the defines clause must not refer to unshared, allocated storage before the function is called. They are completely defined after the function returns. When the function is checked, they are assumed to be undefined at function entrance and an error is reported if there is a path on which they are not defined before the function returns./*@allocates references@*/
References in the allocates clause must not refer to unshared, allocated storage before the function is called. They are allocated but not necessarily defined after the function returns. When the function is checked, they are assumed to be undefined at function entrance and an error is reported if there is a path on which they are not allocated before the function returns./*@releases references@*/
References in the releases clause are deallocated by the function. They must correspond to storage which could be passed as an only parameter before the function is called, and are dead pointers after the function returns. When the function is checked, they are assumed to be allocated at function entrance and an error is reported if they refer to live, allocated storage at any return point.
Additional generic special clauses can be used to describe other aspects of the state of inner storage before or after a call. Generic special clauses have the form state:constraint. The state is either pre (before the function is called), or post (after the function is called). The constraint is similar to an annotation. The following constraints are supported:
Some examples of special clauses are shown in Figure 17. The defines clause for record_new indicates that the id field of the structure pointed to by the result is defined, but the name field is not. So, record_create needs to call record_setName to define the name field. Similarly, the releases clause for record_clearName indicates that no storage is associated with the name field of its parameter after the return, so no failure to deallocate storage message is produced for the call to free in record_free.Aliasing Annotations
pre:only, post:only
pre:shared, post:shared
pre:owned, post:owned
pre:dependent, post:dependent
References refer to only, shared, owned or dependent storage before (pre) or after (post) the call.Exposure Annotations
pre:observer, post:observer
pre:exposed, post:exposed
References refer to observer or exposed storage before (pre) or after (post) the call.Null State Annotations
pre:isnull, post:isnullReferences have the value NULL before (pre) or after (post) the call. Note, this is not the same name or meaning as the null annotation (which means the value may be NULL.)pre:notnull, post:notnullReferences do not have the value NULL before (pre) or after (post) the call.