Contents

1 Operation................................................................................................................ 11

1.1 Warnings............................................................................................................. 11

1.2 Flags.................................................................................................................... 12

1.3 Stylized Comments............................................................................................... 12

1.3.1 Annotations................................................................................................... 13

1.3.2 Setting Flags.................................................................................................. 13

2 Null Dereferences................................................................................................... 14

2.1.1 Predicate Functions........................................................................................ 14

2.1.2 Notnull Annotations........................................................................................ 15

2.1.3 Relaxing Null Checking.................................................................................. 15

3 Undefined Values.................................................................................................... 17

3.1.1 Undefined Parameters................................................................................... 17

3.1.2 Relaxing Checking......................................................................................... 18

3.1.3 Partially Defined Structures............................................................................ 18

4 Types....................................................................................................................... 19

4.1 Built in C Types.................................................................................................... 19

4.1.1 Characters.................................................................................................... 19

4.1.2 Enumerators.................................................................................................. 19

4.1.3 Numeric Types.............................................................................................. 19

4.1.4 Arbitrary Integral Types................................................................................. 19

4.2 Boolean Types..................................................................................................... 20

4.3 Abstract Types..................................................................................................... 21

4.3.1 Controlling Access......................................................................................... 22

4.3.2 Mutability...................................................................................................... 23

4.4 Polymorphism....................................................................................................... 24

5 Memory Management............................................................................................ 25

5.1 Storage Model...................................................................................................... 25

5.2 Deallocation Errors............................................................................................... 26

5.2.1 Unshared References.................................................................................... 26

5.2.2 Temporary Parameters.................................................................................. 27

5.2.3 Owned and Dependent References................................................................. 27

5.2.4 Keep Parameters........................................................................................... 28

5.2.5 Shared References........................................................................................ 28

5.2.6 Stack References.......................................................................................... 28

5.2.7 Inner Storage................................................................................................. 28

5.3 Implicit Memory Annotations................................................................................. 29

5.4 Reference Counting.............................................................................................. 30

6 Sharing.................................................................................................................... 31

6.1 Aliasing................................................................................................................ 31

6.1.1 Unique Parameters........................................................................................ 31

6.1.2 Returned Parameters..................................................................................... 31

6.2 Exposure.............................................................................................................. 32

6.2.1 Read-Only Storage........................................................................................ 32

6.2.2 Exposed Storage............................................................................................ 33

7 Function Interfaces................................................................................................. 35

7.1 Modifications........................................................................................................ 35

7.1.1 State Modifications........................................................................................ 36

7.1.2 Missing Modifies Clauses............................................................................... 36

7.2 Global Variables................................................................................................... 37

7.2.1 Controlling Globals Checking.......................................................................... 37

7.2.2 Definition State.............................................................................................. 38

7.3 Declaration Consistency........................................................................................ 38

7.4 State Clauses....................................................................................................... 39

7.5 Requires and Ensures Clauses............................................................................... 41

8 Control Flow........................................................................................................... 43

8.1 Execution............................................................................................................. 43

8.2 Undefined Behavior.............................................................................................. 44

8.3 Problematic Control Structures.............................................................................. 45

8.3.1 Likely Infinite Loops...................................................................................... 45

8.3.2 Switches....................................................................................................... 46

8.3.3 Deep Breaks................................................................................................. 46

8.3.4 Loop and If Bodies........................................................................................ 47

8.3.5 Complete Logic............................................................................................. 47

8.4 Suspicious Statements........................................................................................... 47

8.4.1 Statements with No Effects............................................................................ 47

8.4.2 Ignored Return Values................................................................................... 48

9 Buffer Sizes............................................................................................................. 49

9.1 Checking Accesses.............................................................................................. 49

9.2 Annotating Buffer Sizes........................................................................................ 49

9.3 Warnings............................................................................................................. 50

10 Extensible Checking............................................................................................ 52

10.1 Defining Attributes............................................................................................ 52

10.2 Annotations...................................................................................................... 54

10.3 Example........................................................................................................... 54

11 Macros.................................................................................................................. 55

11.1 Constant Macros............................................................................................... 55

11.2 Function-like Macros......................................................................................... 55

11.2.1 Side Effect Free Parameters....................................................................... 56

11.3 Controlling Macro Checking............................................................................... 57

11.4 Iterators........................................................................................................... 58

11.4.1 Defining Iterators....................................................................................... 58

11.4.2 Using Iterators........................................................................................... 58

12 Naming Conventions............................................................................................ 60

12.1 Type-Based Naming Conventions...................................................................... 60

12.1.1 Czech Names............................................................................................. 60

12.1.2 Slovak Names............................................................................................ 61

12.1.3 Czechoslovak Names.................................................................................. 61

12.2 Namespace Prefixes......................................................................................... 61

12.3 Naming Restrictions.......................................................................................... 63

12.3.1 Reserved Names........................................................................................ 63

12.3.2 Distinct Names........................................................................................... 63

13 Completeness....................................................................................................... 65

13.1 Unused Declarations......................................................................................... 65

13.2 Complete Programs........................................................................................... 65

13.2.1 Unnecessarily External Names.................................................................... 65

13.2.2 Declarations Missing from Headers............................................................. 65

14 Libraries and Header File Inclusion.................................................................... 66

14.1 Standard Libraries............................................................................................. 66

14.1.1 ISO Standard Library.................................................................................. 66

14.1.2 POSIX Library........................................................................................... 66

14.1.3 UNIX Library............................................................................................ 66

14.1.4 Strict Libraries............................................................................................ 66

14.2 Generating Libraries.......................................................................................... 67

14.2.1 Generating the Standard Libraries................................................................ 67

14.3 Header File Inclusion......................................................................................... 68

14.3.1 Preprocessing Constants............................................................................. 68

Appendix A Availability............................................................................................... 71

Appendix B Flags........................................................................................................ 72

Global Flags................................................................................................................... 72

Help.......................................................................................................................... 72

Initialization................................................................................................................ 72

Pre-processor............................................................................................................ 73

Libraries.................................................................................................................... 73

Output....................................................................................................................... 74

Expected Errors......................................................................................................... 75

Message Format............................................................................................................ 75

Mode Selector Flags....................................................................................................... 75

Checking Flags............................................................................................................... 76

Key........................................................................................................................... 76

Types........................................................................................................................ 76

Function Interfaces..................................................................................................... 79

Memory Management................................................................................................ 81

Sharing...................................................................................................................... 84

Use Before Definition (Section 3)............................................................................... 85

Null Dereferences (Section 2).................................................................................... 85

Macros (Section 7).................................................................................................... 85

Iterators..................................................................................................................... 86

Naming Conventions................................................................................................... 86

Other Checks............................................................................................................. 90

Flag Name Abbreviations................................................................................................ 95

Appendix C Annotations............................................................................................. 97

Suppressing Warnings................................................................................................. 97

Syntactic Annotations..................................................................................................... 97

Functions................................................................................................................... 97

Iterators (Section 11.4)............................................................................................... 98

Constants (Section 11.1)............................................................................................. 98

Alternate Types (Section 4.4)...................................................................................... 98

Declarator Annotations............................................................................................... 98

Type Access.............................................................................................................. 98

Macro Expansion...................................................................................................... 101

Arbitrary Integral Types............................................................................................ 102

Traditional Lint Comments........................................................................................ 102

Metastate Definitions.................................................................................................... 103

Appendix D Specifications ......................................................................................... 104

Specification Flags.................................................................................................... 104

Appendix E Annotated Bibliography........................................................................ 107

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).

2 Null Dereferences

A common cause of program failures is when a null pointer is dereferenced. Splint 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), Splint 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 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 8.1) that check the pointer is not NULL.

Consider two implementations of firstChar in Figure 2. For firstChar1, Splint 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.

null.c

Running Splint

char firstChar1 (/*@null@*/ char *s)

{
3 return *s;

}

char firstChar2 (/*@null@*/ char *s)

{

if (s == NULL) return ‘\0’;
9 return *s;

}

> splint null.c

Splint 3.0.1

null.c: (in function firstChar1)

null.c:3:11: Dereference of possibly null pointer s: *s

null.c:1:35: Storage s may become null

Finished checking --- 1 code warning found

Figure 2. Null Checking

Output from running Splint is displayed in sans-serif font. The command line is preceded by >, the rest is output from Splint. Explanations added to the code or splint output are shown in italics. Code shown in the figures in this document is available from the splint web site, http://www.splint.org . No error is reported for line 9, since the dereference is reached only if s is non-null. For most of the figures, the options -linelen 55 -hints –showcol were used to produce condensed output, and –exportlocal to inhibit warnings about exported declarations.

2.1.1 Predicate Functions

Another way to protect null dereference, is to declare a function using nullwhentrue or falsewhennull(these annotations where originally falsenull and truenull, but were renamed to clarify the logical asymmetry; falsenull and truenull may still be used) and call the function in a conditional statement before the null-annotated pointer is dereferenced.

If a function annotated with nullwhentrue returns true it means its first passed parameter is NULL. If it returns false, the parameter is not NULL. Note that it may return true for a parameter that is not NULL. A more descriptive name for nullwhentrue would be “if the result is false, the parameter was not null”. For example, if isNull is declared as,

/*@nullwhentrue@*/ 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 nullwhentrue annotation this means s must not be null.

The falsewhennull annotation is not quite the logical opposite of nullwhentrue. If a function declared with falsewhennull returns true, it means its parameter is definitely not NULL. If it returns false, the parameter may or may not be NULL. That is a falsewhennull always returns false when passed a NULL parameter; it may sometimes return false when passed a non-NULL parameter.

For example, we could define isNonEmpty to return true if its parameter is not NULL and has least one character before the NUL terminator:

/*@falsewhennull@*/ bool isNonEmpty (/*@null@*/ char *x)

{

return (x != NULL && *x != ‘\0’);

}

Splint does not check that the implementation of a function declared with nullwhentrue or falsewhennull is consistent with its annotation, but assumes the annotation is correct when code that calls the function is checked.

2.1.2 Notnull Annotations

The notnull annotation specifies that a declarator is definitely not NULL. By default, this is assumed, but it may be necessary to use notnull to override a null in a type definition. 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 (see Section 4.3) where the null test has already been done before the function is called, or function results known to never be 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.

2.1.3 Relaxing Null Checking

An additional annotation, relnull may be used to relax null 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. Splint 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.

3 Undefined Values

Like many static checkers, Splint 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. The usedef flag controls use before definition checking.

Splint 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.

3.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.

Splint 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, Splint 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.

Splint reports an error if storage reachable by the caller after the call is not defined when the function returns. This can be suppressed by -must-define. After a call returns, an actual parameter corresponding to an out parameter is assumed to be completely defined.

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.

usedef.c

Running Splint

extern void

setVal (/*@out@*/ int *x);

extern int

getVal (/*@in@*/ int *x);

extern int mysteryVal

(int *x);

int dumbfunc

(/*@out@*/ int *x, int i)

{

if (i > 3)

11 return *x;

else if (i > 1)

13 return getVal (x);

else if (i == 0)

15 return mysteryVal (x);

else

{

18 setVal (x);

19 return *x;

}

> splint usedef.c

usedef.c:11: Value *x used before definition

usedef.c:13: Passed storage x not completely defined

(*x is undefined): getVal (x)

usedef.c:15: Passed storage x not completely defined

(*x is undefined): mysteryVal (x)

Finished checking --- 3 code warnings

No error is reported for line 18, since the incompletely defined storage x is passed as an out parameter. After the call, x may be dereferenced, since setVal is assumed to completely define its out parameter. The warning for line 15 would not appear if +impouts were used since there is no in annotation on the parameter to mysteryVal.

Figure 3. Use before Definition

3.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.

3.1.3 Partially Defined Structures

The partial annotation 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.

4 Types

Strong type checking often reveals programming errors. Splint can check primitive C types more strictly and flexibly than typical compilers (4.1) and provides support a Boolean type (4.2). In addition, users can define abstract types that provide information hiding (0).

4.1 Built in C Types

Two types have compatible type if their types are the same.

ANSI C, 3.1.2.6.

Splint supports stricter checking of built in C types. The char and enum types can be checked as distinct types, and the different numeric types can be type-checked strictly.

4.1.1 Characters

The primitive char type can be type-checked as a distinct type. If char is used as a distinct type, common errors involving assigning ints to chars are detected.

The +charint flag can be used for checking legacy programs where char and int are used interchangeably. If charint is on, char types indistinguishable from ints. To keep char and int as distinct types, but allow chars to be used to index arrays, use +charindex.

4.1.2 Enumerators

Standard C treats user-declared enum types just like integers. An arbitrary integral value may be assigned to an enum type, whether or not it was listed as an enumerator member. Splint checks each user-defined enum type as distinct type. An error is reported if a value that is not an enumerator member is assigned to the enum type, or if an enum type is used as an operand to an ar







Splint - Secure Programming Lint	info@splint.org




Download - Documentation - Manual - Links	Reporting Bugs - Mailing Lists Sponsors - Credits

Authors

Credits