Shape analysis is the process of annotating each program point with an
invariant which describes, the structure of dynamically allocated objects
at this point (independent of the path to that point which was taken).
For example, one possible invariant may be that a pointer variable
points to a doubly linked list.
These invariants are useful for generating more efficient code and for program
understanding.
We describe a new algorithm for shape analysis. The algorithm is parametric,
i.e., it allows to track different classes of invariants using different
parameter settings.
With one parameter setting, our algorithm automatically deduces that
various natural program operations maintain doubly linked lists.
This problem was left open by all the previous methods.
Other setting allows our algorithm to identify lists and unshared objects
in more cases than our previously developed ad-hock shape analysis algorithm.
(This is a joint work with Thomas Reps and Reinhard Wilhelm.)