SPLint is a powerful static analysis tool for C, from University of Virginia's Secure Programming Group.  It began life as a tool to aid in lightweight formal methods development, and it sustains those capabilities in its current incarnation.  While SPLint's powerful analysis can be used to detect defects and issues in any ANSI compliant C source code, its power does not end there.

Other capabilities of SPLint include the ability to check code against LARCH LCL interface declarations (formal methods); to define custom analyses using a simple declarative language; and to create API profiles that enhance analysis for libraries and APIs you work with frequently.  The documentation for SPLint is first rate; although some of the more esoteric features may not be all that obvious at first.  If you intend to use the LCL features you will need further documentation in the syntax of these specifications.  One very good example is the book (now available as a PDF) Introduction to LCL: A Larch/C Interface Language.

One very powerful aspect of SPLint is that it's operation may be integrated with many IDE editors, allowing for a single-keystroke analysis with hyper-linking to issues.  This makes it possible for developers to perform quick check-ups of their code-in-progress, and fix issues before they propagate.

For a more complete look at the features and benefits of employing Splint, please see our whitepaper on the topic.  SPLint is a freely available open-source tool which can be downloaded from the SPLint.org website.   

SafeCode, LLC proudly recommends SPLint and we can provide training and assistance in integrating SPLint into your process.