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.