Static detection of dynamic memory errors

ABSTRACT

Many important classes of bugs result from invalid assumptions about the results of functions and the values of parameters and global variables. Using traditional methods, these bugs cannot be detected efficiently at compile-time, since detailed cross-procedural analyses would be required to determine the relevant assumptions. In this work, we introduce annotations to make certain assumptions explicit at interface points. An efficient static checking tool that exploits these annotations can detect a broad class of errors including misuses of null pointers, uses of dead storage, memory leaks, and dangerous aliasing. This technique has been used successfully to fix memory management problems in a large program.

REFERENCES

• 1: Hans-Juergen Boehm , Mark Weiser, Garbage collection in an uncooperative environment, Software—Practice & Experience, v.18 n.9, p.807-820, September 1988 [doi>10.1002/spe.4380180902]
• 2: D. Evans, Using Specifications to Check Source Code, Massachusetts Institute of Technology, Cambridge, MA, 1994
• 3: David Evans. LCLint User's Guide, Version 2.0. February 1996. (http ://larch-www. lcs.mit.edu:8001/!arch/!clint/guideO
• 4: David Evans , John Guttag , James Horning , Yang Meng Tan, LCLint: a tool for using specifications to check code, Proceedings of the 2nd ACM SIGSOFT symposium on Foundations of software engineering, p.87-96, December 06-09, 1994, New Orleans, Louisiana, United States
• 5: John V. Guttag , James J. Horning, Larch: languages and tools for formal specification, Springer-Verlag New York, Inc., New York, NY, 1993
• 6: Laurie J. Hendren , Joseph Hummell , Alexandru Nicolau, Abstractions for recursive pointer data structures: improving the analysis and transformation of imperative programs, Proceedings of the ACM SIGPLAN 1992 conference on Programming language design and implementation, p.249-260, June 15-19, 1992, San Francisco, California, United States
• 7: Posting in comp. os. linux, August 1994.
• 8: Robert Strom and Nagui Halim. A new programming methodology for long-lived software systems. IBM-RC 9979, IBM T J. Watson Research Center, March 1983.
• 9: Yang Meng Tan. Formal Specification Techniques for Promoting Software Modularity, Enhancing Software Documentation, and Testing Specifications, MIT/LCS/TR-619, MIT Laboratory for Computer Science, June 1994.
• 10: Gray Watson. Debug Malloc Library, November 1994. (ftp ://ftp.letters.com/src/dmalloc/docs/dma!loc. ps)
• 11: Benjamin Zorn and Paul Hilfinger. A memory allocation profiler for C and Lisp programs. (ffp'J/gatokoopor. dec.com:/pbu/mise/mprof-3.0.tar. Z)

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING

Additional Classification:
  B. Hardware
  B.3 MEMORY STRUCTURES

  D. Software
  D.2 SOFTWARE ENGINEERING
  D.4 OPERATING SYSTEMS

General Terms:
Management, Reliability, Verification