2 Another way to provide extra information about code is to use formal specifications (Appendix G).
3 Unlike regular C comments, control comments should not be used within a
single token. They may introduce new separators in the code during parsing.
4 For abstract types whose instances can change value, a client does need to
know if assignment has copy or sharing semantics (see Section 3.2).
5 Does not apply to HTML version.
italics.
6 The meta-notation, item,+ is used to denote a comma separated list of items.
For example, /*@access mstring, intSet@*/ provides access to
the representations of both mstring and intSet.)
7 Through the parameter. Modifications using some other variable that has a
pointer to the location of this parameter are not considered.
8 To change
the names of TRUE and FALSE, use -booltrue
and -boolfalse. The
LCLint distribution includes an implementation of bool, in lib/bool.h.
However, it isn't necessary to use this implementation to get the
benefits of boolean checking.
9 This means that theoreticians can prove that no algorithm exists that solves
the problem correctly for all possible programs.
10 This section is largely based on [Evans96]. It semi-formally defines
some of the terms needed to describe memory management checking; if you are satisfied with an intuitive understanding of these terms, this section may be
skipped.
11 This is similar to the LISP storage model, except that objects are typed.
12 Except sizeof, which does not need the value of its argument.
13 If the storage is not assigned to a reference, an internal reference
is created to track the storage.
14 The full declaration of malloc also includes a null
annotation (Section 7.2) to
indicate that the result may be NULL (as it is when the requested storage
cannot be allocated) and an out annotation (Section 7.1) to indicate that the result
points to undefined storage.
15 The full declaration of free also has out and
null annotations on the parameter to indicate that the argument
may be NULL and need not point to defined storage. According
to [ANSI, 4.10.3.2], NULL may
be passed to free without an error. On some UNIX platforms,
passing NULL to free causes a program crash so the
UNIX version of the standard library (Appendix F) specifies free without the
null annotation on its parameter. To check that allocated
objects are completely destroyed (e.g., all unshared objects inside a
structure are deallocated before the structure is deallocated), LCLint
checks that any parameter passed as an out only void * does not
contain references to live, unshared objects. This makes sense, since
such a parameter could not be used sensibly in any way other than
deallocating its storage.
16 If an exposure qualifier is used (see Section 6.2), the implied dependent
annotation is used instead of the more generally implied only
annotation.
17 Strictly, we should also check that the returned observer storage is not
used again after any other calls to the abstract type module using the same
parameter. LCLint does not attempt to check this, and in practice it is not
usually a problem.
18 Note that if the parameter is annotated with only, it is not an error to
assign it to part of an abstract representation, since the caller may not use
the storage after the call returns.
19 That is, the return type is bool, or int if +boolint is used.
20 The sef annotation denotes a parameter as side-effect free (see Section 8.2.1).
By declaring the argument to assert to be side-effect free, LCLint will report
errors if the parameter to assert produces a side-effect. This is especially
pertinent if assertions are turned off when the production version is compiled.
The bool /*@alt int@*/ type specifier for the parameter means
the parameter type must match either bool or int.
Alternate types are described in Section
8.2.2.
21 To be completely correct, all the macro parameters should be evaluated
before the macro has any side-effects. Since checking this would require
extensive analysis for occasional modest gain, it was not considered worth
implementing.
22 Note that functions which do not produce to the same result each time they
are called with the same arguments should be declared to modify internalState
so they will lead to errors if they are passed as sef parameters.
23 The most renown C naming convention is the Hungarian naming convention,
introduced by Charles Simonyi [Simonyi, Charles, and Martin Heller. "The
Hungarian Revolution." BYTE, August 1991, p. 131-38]. The names for
LCLint naming conventions follow the tradition of using Central European
nationalities as mnemonics for naming conventions. The LCLint conventions are
similar to the Hungarian naming convention in that they encode type information
in names, except that the LCLint conventions encode the names of accessible
abstract types instead of the type of the declaration of return value.
Prefixes used in the Hungarian naming convention are not supported by LCLint.
24 Namespace prefixes should probably be described by regular expressions.
LCLint uses a simpler, more limited means for describing names, which is
believed to be adequate for describing most useful naming conventions. If
there is sufficient interest, regular expressions may be supported in a future
version of LCLint.
25 Peter van der Linden estimates that default fall through is the wrong
behavior 97% of the time. [vdL95, p. 37]
26 "Software Glitch Cripples AT&T Network", Telephony, 22 January 1990.
