Using Specifications to Check Source Code

David Evans
MIT/LCS/TR-628
June 1994

Abstract

Traditional static checkers are limited to detecting simple anomalies since they have no information regarding the intent of the code. Program verifiers are too expensive for nearly all applications. This thesis investigates the possibilities of using specifications to do lightweight static checks to detect inconsistencies between specifications and implementations. A tool, LCLint, was developed to do static checks on C source code using LCL specifications. It is similar to traditional lint, except it uses information in specifications to do more powerful checks. Some typical problems detected by LCLint include violations of abstraction barriers and modifications of caller-visible state that are inconsistent with the specification. Experience using LCLint to check a specified program and to understand and maintain a program with no specifications illustrate some applications of LCLint and suggest future directions for using specifications to check source code.

Full Report (96 pages) [PS]

Splint Project Page


CS 655 David Evans - Publications
University of Virginia
Department of Computer Science
David Evans
evans@cs.virginia.edu