Lecture Notes in Computer Science, 2001, Volume 2027/2001, 133-149, DOI: 10.1007/3-540-45306-7_10

Interprocedural Shape Analysis for Recursive Programs

Noam Rinetzky and Mooly Sagiv

View Related Documents

Abstract

A shape-analysis algorithm statically analyzes a program to determine information about the heap-allocated data structures that the program manipulates. The results can be used to optimize, understand, debug, or verify programs. Existing algorithms are quite imprecise in the presence of recursive procedure calls. This is unfortunate, since recursion provides a natural way to manipulate linked data structures. We present a novel technique for shape analysis of recursive programs. An algorithm based on our technique has been implemented. It handles programs manipulating linked lists written in a subset of C. The algorithm is significantly more precise than existing algorithms. For example, it can verify the absence of memory leaks in many recursive programs; this is beyond the capabilities of existing algorithms.
Partially supported by the Technion and the Israeli Academy of Science.

Fulltext Preview

Image of the first page of the fulltext document