  Biabduction-based shape analysis is a static analysis technique that can find
bugs and ensure memory safety in the presence of complex, linked data
structures. As such, this analysis has proven to be scalable and is implemented
in state-of-the-art industrial-strength analyzers. However, standard
biabduction-based shape analysis requires two analysis phases to guarantee that
all computed function contracts are sound. We introduce two novel techniques
shared learning and shape extrapolation that tackle the soundness problems of
biabduction-based shape analysis and allow for a sound one-phase analysis for
many real-world programs. We formally prove that both techniques guarantee
soundness and verify their effectiveness in a case study based on a prototype
implementation.
