We consider a version of Java with imperative update and explicit deallocation in the style of C / C++. We assume a free-list from which cells are taken upon object creation and to which deallocated objects are returned for future use. Our goal is to automatically infer an upper bound as a function of the input on the size of a free-list required to successfully evaluate a program phrase.
Our analysis uses ideas from amortised complexity and brings interesting aspects having to do with aliasing and circular data structures.
This generalises our previous work on first-order functional programs (POPL2003).