Interprocedural Shape Analysis with TVLA

Bertrand Jeannet, Thomas Reps and Moley Sagiv

May 31, 2006

We give here some experimental results we obtained with an interprocedural version of the TVLA tool. The interprocedural analysis method we use for these experiments has been published as an INRIA research report and submitted to a conference. The analysis method is obtained by abstracting properly sets of stacks in the concrete semantics of programs to sets of activations records. We apply it to shape analysis, using the abstract lattice of 3-valued logical structures as described in TVLA. We assume a knowledge of this analysis.

The experiments were performed on a PC equipped with a 2 GHz Pentium 4 processor and 768 Mb of memory.