[1] Lint is a common programming tool for detecting anomalies in C programs. S. C. Johnson developed the original lint in the late seventies, mainly because early versions of C did not support function prototypes. Splint was originally named LCLint because it was originally intended to check for inconsistencies between LCL specifications and C implementations. To reflect divergence from LCL and increased focus on detecting security vulnerabilities, the name was changed to Splint, short for “Specification Lint” and “Secure Programming Lint”.
[2] The meta-notation, item,+ is used to denote a comma separated list of items. For example, /*@access mstring, intSet@*/
allows access to the representations of both mstring and intSet.)
[3] 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.
[4] This is similar to the LISP storage model, except that objects are typed.
[5] Except sizeof, which does not need the value of its argument.
[6] If the storage is not assigned to a reference, an internal reference is created to track the storage.
[7] The declaration of free has a null annotation on the parameter to indicate that the argument may be NULL. According to [ISO, 7.20.3.2], NULL may be passed to free without no action. On some UNIX platforms, passing NULL to free causes a program crash so the UNIX version of the standard library 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), Splint 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.
[8] In versions of Splint before 3.0, the noreturn annotation was named exits. The noreturn annotation means the same thing, but is a more appropriate name. For legacy code, Splint still supports the exits annotations. Similarly, maynotreturn replaces mayexit, noreturnwhentrue replaces truexit and noreturnwhenfalse replaces falseexit.
[9]The sef annotation denotes a parameter as side effect free (see Section 11.2.1). We use bool /*@alt int@*/ as the type of the parameter, to indicate that it may be either a Boolean or an integer.
[10] Peter van der Linden estimates that default fall through is the wrong behavior 97% of the time. [vdL95, p. 37]
[11] “Software Glitch Cripples AT&T Network”, Telephony, 22 January 1990.
[12] See [Larochelle01] for information on internal aspects of the checking.
[13] This section is largely based on [Evans02].
[14] C. Cowan et al., FormatGuard: Automatic Protection from printf Format String Vulnerabilities. 10th Usenix Security Symposium, 2001.
[15] To be completely correct, all the macro parameters should be evaluated before the macro has any side effects. Splint does not check this.
[16] Functions that 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.
[17] The most renowned 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 Splint naming conventions follow the tradition of using Central European nationalities as mnemonics for naming conventions. The Splint conventions are similar to the Hungarian naming convention in that they encode type information in names, except that the Splint 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 Splint.
[18] Of course, namespace prefixes should really be described by regular expressions. If there is sufficient interest (that is, someone volunteers to program it), regular expressions will be supported in a future version of Splint.
[19] POSIX library was contributed by Jens Schweikhardt.