Splint Manual

Version 3.1.1-1

5 June 2003

 

Authors and Credits
Secure Programming Group
University of Virginia, Department of Computer Science

Contents

1����� Operation

1.1���� Warnings

1.2���� Flags

1.3���� Stylized Comments

1.3.1���� Annotations

1.3.2���� Setting Flags

2����� Null Dereferences

2.1.1���� Predicate Functions

2.1.2���� Notnull Annotations

2.1.3���� Relaxing Null Checking

3����� Undefined Values

3.1.1���� Undefined Parameters

3.1.2���� Relaxing Checking

3.1.3���� Partially Defined Structures

4����� Types

4.1���� Built in C Types

4.1.1���� Characters

4.1.2���� Enumerators

4.1.3���� Numeric Types

4.1.4���� Arbitrary Integral Types

4.2���� Boolean Types

4.3���� Abstract Types

4.3.1���� Controlling Access

4.3.2���� Mutability

4.4���� Polymorphism

5����� Memory Management

5.1���� Storage Model

5.2���� Deallocation Errors

5.2.1���� Unshared References

5.2.2���� Temporary Parameters

5.2.3���� Owned and Dependent References

5.2.4���� Keep Parameters

5.2.5���� Shared References

5.2.6���� Stack References

5.2.7���� Inner Storage

5.3���� Implicit Memory Annotations

5.4���� Reference Counting

6����� Sharing

6.1���� Aliasing

6.1.1���� Unique Parameters

6.1.2���� Returned Parameters

6.2���� Exposure

6.2.1���� Read-Only Storage

6.2.2���� Exposed Storage

7����� Function Interfaces

7.1���� Modifications

7.1.1���� State Modifications

7.1.2���� Missing Modifies Clauses

7.2���� Global Variables

7.2.1���� Controlling Globals Checking

7.2.2���� Definition State

7.3���� Declaration Consistency

7.4���� State Clauses

7.5���� Requires and Ensures Clauses

8����� Control Flow

8.1���� Execution

8.2���� Undefined Behavior

8.3���� Problematic Control Structures

8.3.1���� Likely Infinite Loops

8.3.2���� Switches

8.3.3���� Deep Breaks

8.3.4���� Loop and If Bodies

8.3.5���� Complete Logic

8.4���� Suspicious Statements

8.4.1���� Statements with No Effects

8.4.2���� Ignored Return Values

9����� Buffer Sizes

9.1���� Checking Accesses

9.2���� Annotating Buffer Sizes

9.3���� Warnings

10����� Extensible Checking

10.1������ Defining Attributes

10.2������ Annotations

10.3������ Example

11����� Macros

11.1������ Constant Macros

11.2������ Function-like Macros

11.2.1������ Side Effect Free Parameters

11.3������ Controlling Macro Checking

11.4������ Iterators

11.4.1������ Defining Iterators

11.4.2������ Using Iterators

12����� Naming Conventions

12.1������ Type-Based Naming Conventions

12.1.1������ Czech Names

12.1.2������ Slovak Names

12.1.3������ Czechoslovak Names

12.2������ Namespace Prefixes

12.3������ Naming Restrictions

12.3.1������ Reserved Names

12.3.2������ Distinct Names

13����� Completeness

13.1������ Unused Declarations

13.2������ Complete Programs

13.2.1������ Unnecessarily External Names

13.2.2������ Declarations Missing from Headers

14����� Libraries and Header File Inclusion

14.1������ Standard Libraries

14.1.1������ ISO Standard Library

14.1.2������ POSIX Library

14.1.3������ UNIX Library

14.1.4������ Strict Libraries

14.2������ Generating Libraries

14.2.1������ Generating the Standard Libraries

14.3������ Header File Inclusion

14.3.1������ Preprocessing Constants

Appendix A��� Availability

Appendix B��� Flags

Global Flags

Help

Initialization

Pre-processor

Libraries

Output

Expected Errors

Message Format

Mode Selector Flags

Checking Flags

Key

Types

Function Interfaces

Memory Management

Sharing

Use Before Definition (Section 3)

Null Dereferences (Section 2)

Macros (Section 7)

Iterators

Naming Conventions

Other Checks

Flag Name Abbreviations

Appendix C��� Annotations

Suppressing Warnings

Syntactic Annotations

Functions

Iterators (Section 11.4)

Constants (Section 11.1)

Alternate Types (Section 4.4)

Declarator Annotations

Type Access

Macro Expansion

Arbitrary Integral Types

Traditional Lint Comments

Metastate Definitions

Appendix D��� Specifications

Specification Flags

Appendix E��� Annotated Bibliography

Index

 

Figures

 

Figure 1.� Typical Effort-Benefit Curve for Using Splint

Figure 2.� Null Checking

Figure 3.� Use before Definition

Figure 4.� Boolean Checking

Figure 5.� Information Hiding Violations

Figure 6.� Memory Management

Figure 7.� Stack-Allocated Storage

Figure 8.� Implicit Annotations

Figure 9.� Reference Counting

Figure 10.� Unique parameters

Figure 11.� Exposure

Figure 12.� Modification

Figure 13.� Global Variables

Figure 14.� Annotated Globals Lists

Figure 15.� State Clauses

Figure 16.� Evaluation Order

Figure 17.� Infinite Loops

Figure 18.� Switch Cases

Figure 19.� Statements with No Effect

Figure 20.� Ignored Return Values

Figure 21.� Prefix Character Codes

Figure 22.� Distinct Names

Figure 23.� Flag Name Abbreviations