  We investigate the complexity consequences of adding pointer arithmetic to
separation logic. Specifically, we study extensions of the points-to fragment
of symbolic-heap separation logic with various forms of Presburger arithmetic
constraints.
  Most significantly, we find that, even in the minimal case when we allow only
conjunctions of simple "difference constraints" (x'\leq x+k) where k is an
integer, polynomial-time decidability is already impossible: satisfiability
becomes NP-complete, while quantifier-free entailment becomes coNP-complete and
quantified entailment becomes P2-complete (P2 is the second class in the
polynomial-time hierarchy)
  In fact we prove that the upper bound is the same, P2, even for the full
pointer arithmetic but with a fixed pointer offset, where we allow any Boolean
combinations of the elementary formulas (x'=x+k0), (x'\leq x+k0), and
(x'<x+k0), and, in addition to the points-to formulas, we allow spatial
formulas of the arrays the length of which is bounded by k0 and lists which
length is bounded by k0, etc, where k0 is a fixed integer.
  However, if we allow a significantly more expressive form of pointer
arithmetic - namely arbitrary Boolean combinations of elementary formulas over
arbitrary pointer sums - then the complexity increase is relatively modest for
satisfiability and quantifier-free entailment: they are still NP-complete and
coNP-complete respectively, and the complexity appears to increase drastically
for quantified entailments.
