It is pointless to point in bounded heaps

•We model a program with recursive procedure, local variables dynamic allocation and deallocation.•We give an abstraction of the memory model that is precise and finitary.•we show that adding pointer fields does not add any expressiveness if heaps are bounded.

In this paper we introduce a new symbolic semantics for a class of recursive programs which feature dynamic creation and unbounded allocation of objects. We use a symbolic representation of the program state in terms of equations to model the semantics of a program as a pushdown system with a finite set of control states and a finite stack alphabet. Our main technical result is a rigorous proof of the equivalence between the concrete and the symbolic semantics.Adding pointer fields gives rise to a Turing complete language. However, under the assumption that the number of reachable objects in the visible heap is bounded in all the computations of a program with pointers, we show how to construct a program without pointers that simulates it. Consequently, in the context of bounded visible heaps, programs with pointers are no more expressive than programs without them.We conclude by extending programs with a dynamic deallocation statement, an operation that affects all aliases of a deallocated object. We show how to extend the concrete and the symbolic semantics so to retain the previous equivalence result.