LCLint User's Guide - Section 7: Value Constraints

	Guide Contents 1. Overview 2. Operation 3. Abstract Types	4. Function Interfaces 5. Memory Management 6. Sharing 7. Value Constraints	8. Macros 9. Naming Conventions 10. Other Checks Contact: lclint@cs.virginia.edu
This guide is preserved to maintain old links, but has been replaced by the Splint Manual.

7. Value Constraints
LCLint can be used to constrain values of parameters, function results, global variables, and derived storage such as structure fields. These constraints are checked at interface points -- where a function is called or returns. Section 7.1 describes how to constrain parameters, return values and structures to detect use before definition errors. A similar approach is used for restricting the use of possibly null pointers in Section 7.2. To do both well, and avoid spurious errors, information about when and if a function returns if useful. Annotations for documenting execution control are described in Section 7.3.

7.1 Use Before Definition
Like many static checkers, LCLint detects instances where the value of a location is used before it is defined. This analysis is done at the procedural level. If there is a path through the procedure that
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.

7.2.1 Predicate Functions
Another way to protect null dereference, is to declare a function using falsenull or truenull and call the function in a conditional statement before the null-annotated pointer is dereferenced. The falsenull and truenull annotations may only be used on return values for functions that return a boolean[19] result and whose first argument is a possibly null pointer.

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.2 Overriding Null Types
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 where the null test has already been done before the function is called, or function results of the type which are never 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.

Figure 16. Using notnull.

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);
   *x = 3;
is checked correctly, since the falseexit annotation on assert means the deference of x is not reached is x != NULL is false.
7.4 Special Clauses
Sometimes it is necessary to specify function interfaces at a lower level than is possible with the standard annotations. For example, if a function defines some fields of a returned structure but does not define all the fields. The /*@special@*/ annotation is used to mark a parameter, global variable, or return value that is described using special clauses. The usual implicit definition rules do not apply to a special declaration.
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:

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:isnull
References 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:notnull
References do not have the value NULL before (pre) or after (post) the call.

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.
Next: Macros
Contents

This guide is preserved to maintain old links, but has been replaced by the Splint Manual.
	Guide Contents 1. Overview 2. Operation 3. Abstract Types	4. Function Interfaces 5. Memory Management 6. Sharing 7. Value Constraints	8. Macros 9. Naming Conventions 10. Other Checks Contact: lclint@cs.virginia.edu