Biabduction-based shape analysis verifies memory safety of open programs in an efficient compositional way and is applicable even for code fragments without a need for modelling their environment. Nevertheless, the technique suffers from two fundamental problems that were already described upon its introduction by Calcagno et al. (2009), namely dealing with unsound abduction results in indeterminately branching code and with unsound over-approximation within loop acceleration. Together, these problems facilitate the need for a second analysis phase to filter out unsound pre-conditions. In contrast, we introduce novel techniques that overcome the two problems and compute sound analysis results within a single analysis phase.