  We propose a hierarchical abstract domain for the analysis of free-list
memory allocators that tracks shape and numerical properties about both the
heap and the free lists. Our domain is based on Separation Logic extended with
predicates that capture the pointer arithmetics constraints for the heap-list
and the shape of the free-list. These predicates are combined using a
hierarchical composition operator to specify the overlapping of the heap-list
by the free-list. In addition to expressiveness, this operator leads to a
compositional and compact representation of abstract values and simplifies the
implementation of the abstract domain. The shape constraints are combined with
numerical constraints over integer arrays to track properties about the
allocation policies (best-fit, first-fit, etc). Such properties are out of the
scope of the existing analyzers. We implemented this domain and we show its
effectiveness on several implementations of free-list allocators.
