Solving Shape-Analysis Problems in Languages with Destructive Updating
Mooly Sagiv, Thomas Reps, and Reinhard Wilhelm
This paper concerns the static analysis of programs that perform
destructive updating on heap-allocated storage.
We give an algorithm that conservatively solves this problem by using
a finite shape-graph to approximate the possible ``shapes'' that
heap-allocated structures in a program can take on.
In contrast with previous work, our method is even accurate for
certain programs that update cyclic data structures.
For example, our method can determine that when the input to a program
that searches a list and splices in a new element is a possibly
circular list, the output is a possibly circular list.
(Click here to access the paper:
PostScript,
PDF.)