Splint Manual
Version 3.1.1
27 April 2003
Secure Programming Group
University of Vir
g
inia
Department of Computer Science
Splint Manual
2
Authors
This manual was written by David Evans, except for Section 9 and Appendix B which were
written by David Larochelle and David Evans.
Credits
Splint is developed and maintained by the Secure Programming Group at the University of
Virginia Department of Computer Science. David Evans is the project leader and the primary
developer of Splint. David Larochelle developed the memory bounds checking. University of
Virginia students Chris Barker, David Friedman, Mike Lanouette and Hien Phan all contributed
significantly to the development of Splint.
Splint is the successor to LCLint, a tool originally developed as a joint research project between
the Massachusetts Institute of Technology and Digital Equipment Corporation’s System
Research Center. David Evans was the primary designed and developer of LCLint. John
Guttag and Jim Horning had the original idea for a static checking tool for detecting
inconsistencies between LCL specifications and their C implementations. They provided
valuable advice on its functionality and design and were instrumental in its development.
Splint incorporates the original LCL checker developed by Yang Meng Tan. This was built on
the DECspec Project (Joe Wild, Gary Feldman, Steve Garland, and Bill McKeeman). The LSL
checker used by LCLint was developed by Steve Garland. The original C grammar for LCLint
was provided by Nate Osgood. This work has also benefited greatly from discussions with
Mike Burrows, Stephen Garland, Colin Godfrey, Steve Harrison, Yanlin Huang, Daniel
Jackson, John Knight, David Larochelle, Angelika Leeb, Ulana Legedza, Gary McGraw, Anya
Pogosyants, Avneesh Saxena, Seejo Sebastine, Navneet Singh, Raymie Stata, Yang Meng Tan,
and Mark Vandevoorde. I especially thank Angelika Leeb for many constructive comments on
improving an early version of this document, Raymie Stata and Mark Vandevoorde for
technical assistance, and Dorothy Curtis, Paco Hope, Scott Ruffner, Christina Jackson, David
Ladd, and Jessica Greer for systems assistance.
Much of Splint’s development has been driven by feedback from users in academia and
industry. Many more people than I can mention here have made contributions by suggesting
improvements, reporting bugs, porting early versions of Splint to other platforms. Particularly
heroic contributions have been made by Nelson Beebe, Eric Bloodworth, Jutta Degener, Rick
Farnbach, Chris Flatters, Huver Hu, Alexander Mai, John Gerard Malecki, Thomas G.
McWilliams, Michael Meskes, Richard O’Keefe, Jens Schweikhardt, Albert L. Ting and Jim
Zelenka. Martin “Herbert” Dietze and Mike Smith performed valiantly in producing the
original Win32 and OS2 ports. Tim Van Holder produced the
automake and autoconf
distribution.
Splint research at the University of Virginia is currently funded in part by an NSF CAREER
Award and an NSF CCLI Award for using analysis to teach software engineering. Splint has
been previously supported by a grant from NASA and David Larochelle was funded by a
USENIX student research grant.
UVA Secure Programming Group
3
Contents
1 Operation...........................................................................................................................11
1.1 Warnings.......................................................................................................................11
1.2 Flags .............................................................................................................................12
1.3 Stylized Comments.......................................................................................................12
1.3.1 Annotations ...........................................................................................................12
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.3.3 Semi-Abstract Types .............................................................................................24
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....................................................................................................27
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 ......................................................................................................29
6 Sharing...............................................................................................................................31
Splint Manual
4
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......................................................................................................................42
8.1 Execution......................................................................................................................42
8.2 Undefined Behavior......................................................................................................43
8.3 Problematic Control Structures ....................................................................................44
8.3.1 Likely Infinite Loops.............................................................................................44
8.3.2 Switches ................................................................................................................45
8.3.3 Deep Breaks ..........................................................................................................45
8.3.4 Loop and If Bodies................................................................................................46
8.3.5 Complete Logic .....................................................................................................46
8.4 Suspicious Statements ..................................................................................................46
8.4.1 Statements with No Effects ...................................................................................46
8.4.2 Ignored Return Values ..........................................................................................47
9 Buffer Sizes ........................................................................................................................48
9.1 Checking Accesses .......................................................................................................48
9.2 Annotating Buffer Sizes ...............................................................................................48
9.3 Less Stringent Checking...............................................................................................49
9.4 Warnings.......................................................................................................................49
10 Extensible Checking.......................................................................................................52
10.1 Defining Attributes ...................................................................................................52
10.2 Annotations...............................................................................................................54
11 Macros.............................................................................................................................55
11.1 Constant Macros .......................................................................................................55
11.2 Function-like Macros................................................................................................55
UVA Secure Programming Group
5
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................................................................................................67
14.3.1 Preprocessing Constants ....................................................................................68
Appendix A Availability .......................................................................................................69
Appendix B Flags ..................................................................................................................70
Key ..........................................................................................................................................70
Flag Name Abbreviations ...................................................................................................70
Global Flags ............................................................................................................................71
Help.....................................................................................................................................71
Initialization ........................................................................................................................71
Pre-processor.......................................................................................................................72
Libraries ..............................................................................................................................72
Output .................................................................................................................................73
Expected Errors...................................................................................................................74
Message Format ......................................................................................................................74
评论0