Splint Examples

db: Employee Database Program

Starts with a fully specified, complete implementation. Uses LCLint to detect some bugs in the code, detect errors in the specifications, improve the specifications, and adopt and check conformance to a naming convention.

Splint's own source code, of course, is annotated and checked using Splint. [Download Code]

For more examples using Splint, see:

Improving Security Using Extensible Lightweight Static Analysis

David Evans and David Larochelle. In IEEE Software, Jan/Feb 2002. (PDF, 12 pages)

Statically Detecting Likely Buffer Overflow Vulnerabilities

David Larochelle and David Evans. In 2001 USENIX Security Symposium, Washington, D. C., August 13-17, 2001. (PDF, HTML, 13 pages)

Static Detection of Dynamic Memory Errors

David Evans. In SIGPLAN Conference on Programming Language Design and Implementation (PLDI '96), Philadelphia, PA, May 1996.

LCLint: A Tool for Using Specifications to Check Code

David Evans, John Guttag, Jim Horning and Yang Meng Tan, SIGSOFT Symposium on the Foundations of Software Engineering, December 1994.

Using Specifications to Check Source Code

David Evans, MIT/LCS/TR-628, June 1994, SM Thesis.

	Splint - Secure Programming Lint [email protected] Download - Documentation - Manual - Links Source - Linux - Publications - Talks Reporting Bugs    Sponsors - Credits