LCLint User's Guide

Version 2.1a Supplement
18 April 1996

David Evans
University of Virginia, Computer Science Group
MIT Laboratory for Computer Science

This is a supplement to the LCLint User's Guide describing changes between Version 2.0 and Version 2.1a. These sections are also included in the LCLint User's Guide, Version 2.1a.

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.

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.

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.

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.

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.

Include Semantics

The standard behavior of LCLint on encountering

   #include <X.h>

Processing header files on gcc systems may require the +gnuextensions flag. This causes LCLint to support some of the gcc extensions including __asm__, __attribute__ and alternate keywords.

Arbitrary Integral Types

In LCLint 2.0, the standard library types size_t, ptr_diff and wchar_t were declared to have type long unsigned. In fact, the standard does not constrain their types other than limiting them to integral types. In LCLint 2.1a, an arbitrary integral type is used to represent these library types. The matchanyintegral, longintegral, and longunsignedanyintegral flags control type checking for the arbitrary integral type. If none of these flags is on, a type mismatch is reported anywhere an arbitrary integral type is used where a specific (possibly inconsistent) integral type is expected.

Flags

File Inclusion, Parsing

plain: +
systemdirexpandmacros

Expand macros in system directories regardless of other settings, except for macros corresponding to names defined in a load library.

plain: -
continuecomment

A line continuation marker (\) appears inside a comment on the same line as the comment close. Preprocessors should handle this correctly, but it causes problems for some preprocessors. plain: +
duplicatequals

Report duplicate type qualifiers (e.g., long long). Duplicate type qualifiers not supported by ANSI, but some compilers (e.g., gcc) do support duplicate qualifiers.

plain: -
gnuextensions

Support some GNU (gcc) language extensions.

plain: +
unrecogcomments

Stylized comment is unrecognized.

Type Checking

plain: +
charintliteral

A character constant may be used as an int.

plain: -
longintegral

Allow long type to match an arbitrary integral type (e.g., size_t).

m: +---
longunsignedintegral

Allow long unsigned type to match an arbitrary integral type (e.g., size_t).

plain: -
matchanyintegral

Allow any integral type to match an arbitrary integral type (e.g., size_t).

Memory Transfers

m: --++
staticinittrans

Static storage is used as an initial value in an inconsistent way.

m: --++
unqualifiedinittrans

Unqualified storage is used as an initial value in an inconsistent way.