Splint User’s Manual
Version 3.1.1
27 April 2003
Splint[1] is a tool for statically checking C programs for security vulnerabilities and programming mistakes. Splint does many of the traditional lint checks including unused declarations, type inconsistencies, use before definition, unreachable code, ignored return values, execution paths with no return, likely infinite loops, and fall through cases. More powerful checks are made possible by additional information given in source code annotations. Annotations are stylized comments that document assumptions about functions, variables, parameters and types. In addition to the checks specifically enabled by annotations, many of the traditional lint checks are improved by exploiting this additional information.
As more effort is put into annotating programs, better checking results. A representational effort-benefit curve for using Splint is shown in Figure 1. Splint is designed to be flexible and allow programmers to select appropriate points on the effort-benefit curve for particular projects. As different checks are turned on and more information is given in code annotations the number of bugs that can be detected increases dramatically.
Problems detected by Splint include:
· Dereferencing a possibly null pointer (Section 2);
· Using possibly undefined storage or returning storage that is not properly defined (Section 3);
· Type mismatches, with greater precision and flexibility than provided by C compilers (Section 4.1–4.2);
· Violations of information hiding (Section 4.3);
· Memory management errors including uses of dangling references and memory leaks (Section 5);
· Dangerous aliasing (Section 6);
· Modifications and global variable uses that are inconsistent with specified interfaces (Section 7);
· Problematic control flow such as likely infinite loops (Section 8.3.1), fall through cases or incomplete switches (Section 8.3.2), and suspicious statements (Section 8.4);
· Buffer overflow vulnerabilities (Section 9);
· Dangerous macro implementations or invocations (Section 11); and
· Violations of customized naming conventions. (Section 12).
Figure 1. Typical Effort-Benefit Curve
Splint checking can be customized to select what classes of errors are reported using command line flags and stylized comments in the code. In addition, users can define new annotations and associated checks to extend Splint’s checking or to enforce application specific properties (Section 10).
About This Document
This document is a guide to using Splint. Section 1 explains how to run Splint, interpret messages and control checking. Sections 2–13 describe particular checks done by Splint. There are some minor dependencies between sections, but in general they can be read in any order. Section 14 covers issues involving libraries and header file inclusion important for running Splint on large systems.
This document does not describe technical details of the checking. For technical background and analysis of Splint’s effectiveness in practice, see the papers available at http://www.splint.org.
|
Since human beings themselves are not fully debugged yet, there will be bugs in your code no matter what you do. Chris Mason,Zero-defects memo (quoted in Microsoft Secrets, Cusumano and Selby) |
1 Operation
Splint is invoked by listing files to be checked. Initialization files, command line flags, and stylized comments may be used to customize checking globally and locally.
The best way to learn to use Splint, of course, is to actually use it (if you don’t already have Splint installed on your system, see Appendix A). Before you read much further in this document, I recommend finding a small C program. Then, try running:
splint *.c
For the most C programs, this will produce a large number of warnings. To turn off reporting for some of the warnings, try:
splint -weak *.c
The -weak flag is a mode flag that sets many checking parameters to select weaker checking than is done in the default mode. Other Splint flags will be introduced in the following sections; a complete list is given in Appendix B.
1.1 Warnings
A typical warning message is:
sample.c: (in function faucet)
sample.c:11:12 : Fresh storage x not released before return
A memory leak has been detected. Storage allocated locally is not released
before the last reference to it is lost. (Use -mustfreefresh to inhibit
warning)
sample.c:5:47: Fresh storage x allocated
The first line gives the name of the function in which the error is found. This is printed before the first message reported for a function. The second line is the text of the message. This message reports a memory leak—storage allocated in a function is not deallocated before the function returns. The file name, line and column number where the error is located precedes the text.
The next line is a hint giving more information about the suspected error, including information on how the warning message may be suppressed. For this message, using the ‑mustfreefresh flag would prevent this warning from being reported. This flag can be set at the command line, or more precisely just around the code point in question by using annotations (see Section 1.3.2).
The final line of the message gives additional location information. For this message, it tells where the leaking storage was allocated.
The generic message format is (parts enclosed in square brackets are optional):
[<file>:<line> (in <context>)]
<file>:<line>[,<column>]: message
[hint]
<file>:<line>,<column>: extra location information, if appropriate
Users can customize the format and content of messages printed by Splint. The function context is not printed if -showfunc is used. Column numbers are not printed if ‑showcol is used. The +parenfileformat flag can be used to generate file locations in the format recognized by Microsoft Visual Studio. If +parenfileformat is set, the line number follows the file name in parentheses (e.g., sample.c(11).) Messages are split into lines of length less than the value set using -linelen <number>. The default line length is 80 characters. Splint attempts to split lines in a sensible place as near to the line length limit as possible.
The ‑hints prevents any hints from being printed. Normally, a hint is given only the first time a class of error is reported. To have Splint print a hint for every message regardless, use +forcehints.
1.2 Flags
So that many programming styles can be supported, Splint provides several hundred flags for controlling checking and message reporting. Some of the flags are introduced in the body of this document. Appendix B describes every flag. Modes and shortcut flags are provided for setting many flags at once. Individual flags can override the mode settings.
Flags are preceded by + or -. When a flag is preceded by + we say it is on; when it is preceded by - it is off. The precise meaning of on and off depends on the type of flag.
The +/- flag settings are used for consistency and clarity, but contradict standard UNIX usage and it is easy to accidentally use the wrong one. To reduce the likelihood of using the wrong flag, Splint issues warnings when a flag is set in an unusual way. Warnings are issued when a flag is redundantly set to the value it already had (these errors are not reported if the flag is set using a stylized comment), if a mode flag or special flag is set after a more specific flag that will be set by the general flag was already set, if value flags are given unreasonable values, of if flags are set in an inconsistent way. The -warnflags flag suppresses these warnings.
Default flag settings will be read from ~/.splintrc if it is readable. If there is a .splintrc file in the working directory, settings in this file will be read next and its settings will override those in ~/.splintrc. Command-line flags override settings in either file. The syntax of the .splintrc file is the same as that of command-line flags, except that flags may be on separate lines and the # character may be used to indicate that the remainder of the line is a comment. The -nof flag prevents the ~/.splintrc file from being loaded. The -f <filename> flag loads options from filename.
To make flag names more readable, hyphens (-), underscores (_) and spaces in flags at the command line are ignored. Hence, warnflags, warn-flags and warn_flags all select the warnflags option.
1.3 Stylized Comments
Stylized comments are used to provide extra information about a type, variable or function interface to improve checking, or to control flag settings locally.
All stylized comments begin with /*@ and are closed by the end of the comment. The role of the @ may be played by any printable character. Use -commentchar <char> to select a different stylized comment marker.
1.3.1 Annotations
Annotations are stylized comments that follow a definite syntax. Although they are comments, they may only be used in fixed grammatical contexts (e.g., like a type qualifier).
Sections 2–6 describe annotations for expressing assumptions about variables, parameters, return values, structure fields and type definitions. For example, /*@null@*/ is used to express an assumption that a parameter may be NULL. Section 7 describes annotations for describing function interfaces. Other annotations are described in later sections and Section 10 describes mechanisms users can employ to define new annotations. A summary of annotations is found in Appendix C.
Some annotations, known as control comments, may appear between any two tokens in a C program (unlike regular C comments, control comments should not be used within a single token as they introduce new separators in the code). Syntactically, they are no different from standard comments. Control comments are used to provide source-level control of Splint checking. They may be used to suppress spurious messages, set flags, and control checking locally in other ways.
1.3.2 Setting Flags
Most flags (all except those characterized as “global” in Appendix B) can be set locally using control comments. A control comment can set flags locally to override the command line settings. The original flag settings are restored before processing the next file. The syntax for setting flags in control comments is the same as that of the command line, except that flags may also be preceded by = to restore their setting to the original command-line value. For instance,
/*@+charint -modifies=showfunc@*/
sets charint on (this makes char and int indistinguishable types), sets modifies off (this prevents reporting of modification errors), and sets showfunc to its original setting (this controls whether or not the name of a function is displayed before a message).
Next: 2. Null Dereferences
Return to Contents
