Splint - Secure Programming Lint
info@splint.org
Manual Contents - Other Formats Section: 1  2  3  4  5  6  7  8  9  10  11  12  13  14  A  B  C  D  E     Sponsors - Credits

Authors

This manual was written by David Evans, except for Section 9, which was 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, 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 a grant from the NASA Langley Research Center, an NSF CAREER Award for swarm programming, and an NSF CCLI Award for using analysis to teach software engineering.  David Larochelle is funded by a USENIX student research grant.  

Splint Manual
info@splint.org
1. Operation - 2. Null Dereferences - 3. Undefined Values - 4. Types - 5. Memory Management - 6. Sharing
7. Function Interfaces - 8. Control Flow - 9. Buffer Sizes - 10. Extensible Checking - 11. Macros
12. Naming Conventions - 13. Completeness - 14. Libraries and Header File Inclusion
Appendices: A. Availability - B. Flags - C. Annotations - D. Specifications - E. Annotated Bibliography - Index