Using Specifications to Check Source Code
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]
