Lecture Notes in Computer Science, 2006, Volume 4134/2006, 240-260, DOI: 10.1007/11823230_16

Interprocedural Shape Analysis with Separated Heap Abstractions

Alexey Gotsman, Josh Berdine and Byron Cook

View Related Documents

Abstract

We describe an interprocedural shape analysis that makes use of spatial locality (i.e. the fact that most procedures modify only a small subset of the heap) in its representation of abstract states. Instead of tracking reachability information directly and aliasing information indirectly, our representation tracks reachability indirectly and aliasing directly. Computing the effect of procedure calls and returns on an abstract state is easy because the representation exhibits spatial locality mirroring the locality that is present in the concrete semantics. The benefits of this approach include improved speed, support for programs that deallocate memory, the handling of bounded numbers of heap cutpoints, and support for cyclic and shared data structures.

Fulltext Preview

Image of the first page of the fulltext document