  Shape analysis is of great importance for the verification of the correctness
and memory-safety of heap-manipulating programs, yet such analyses have been
shown to be highly difficult problems. The integration of separation logic into
shape analyses has improved the effectiveness of the techniques, but the most
significant advancement in this area is bi-abductive inference. Enabled by
separation logic, bi-abduction - a combination of abductive inference and frame
inference - is the key enabler for compositional reasoning, helping to scale up
verification significantly. Indeed, the success of bi-abduction has led to the
development of Infer, the tool used daily to verify Facebook's codebase of
millions of lines of code. However, this success currently stays largely within
the shape domain. To extend this impact towards the combination of shape and
arithmetic domains, in this work, we present a novel one-stage bi-abductive
procedure for a combination of data structures and ordering values. The
procedure is designed in the spirit of the Unfold-and-Match paradigm where the
inference is utilized to derive any mismatched portion. We have also
implemented a prototype solver, based on the Cyclist library, and demonstrate
its capabilities over a range of benchmarks from the SL-COMP competition. The
experimental results show that our proposal shows promise for the specification
inference in an automated verification of heap-manipulating programs.
