Pointer arithmetic is widely used in memory allocators. Moreover, heap list is a data structure used in many memory allocators, to describe the layout of the physical memory.
Heap list is a data structure used by many implementations of memory allocators
to organize the heap part of the program's memory.
%
%The verification of such programs usually requires simultaneous reasoning about pointer arithmetic and unbounded heap regions.
The specification of the programs in memory allocators usually requires using pointer arithmetic inside inductive definitions to define heap lists. % in memory allocators.
Operations on heap lists employ pointer arithmetics and therefore,
reasoning about the correctness of heap list implementations requires
to deal simultaneously with pointer arithmetic inside the inductive definition
specifying the heap list.
%
In this work, we investigate decision problems for SLAH, a separation logic fragment
that allows pointer arithmetic and an inductive definition for heap lists,
