  Pointer arithmetic is widely used in low-level programs, e.g. memory
allocators. The specification of such programs usually requires using pointer
arithmetic inside inductive definitions to define the common data structures,
e.g. heap lists in memory allocators. In this work, we investigate decision
problems for SLAH, a separation logic fragment that allows pointer arithmetic
inside inductive definitions, thus enabling specification of properties for
programs manipulating heap lists. Pointer arithmetic inside inductive
definitions is challenging for automated reasoning. We tackle this challenge
and achieve decision procedures for both satisfiability and entailment of SLAH
formulas. The crux of our decision procedure for satisfiability is to compute
summaries of inductive definitions. We show that although the summary is
naturally expressed as an existentially quantified non-linear arithmetic
formula, it can actually be transformed into an equivalent linear arithmetic
formula. The decision procedure for entailment, on the other hand, has to match
and split the spatial atoms according to the arithmetic relation between
address variables. We report on the implementation of these decision procedures
and their good performance in solving problems issued from the verification of
building block programs used in memory allocators.
