In the seminal paper that introduced separation logic, John C. Reynolds (2002) writes: “Finally, we give axiom schemata for the predicate ‘‘points to’’. Regrettably, these are far from complete.” Although separation logic has been studied more than twenty years and has seen important applications in industry (Microsoft, Amazon, Meta), never before was completeness of separation logic fully understood—causing costly memory safety errors in practice (cf. the CrowdStrike incident). In fact, the 2016 EATCS Gödel prize winners Stephen Brookes and Peter O’Hearn (famous for Concurrent Separation Logic) write: “It is all too easy to get caught up in completeness and related issues for formal systems that turn out to be too complicated when humans try to apply them; it is more important first to get a sense for the extent to which simple reasoning is or is not supported.” The latter has indeed been demonstrated now, so it is finally time to get caught up in completeness and related issues. In this talk we explain a full characterization of the ‘‘points to’’ predicate of separation logic, thus resolving the first issue. We furthermore present a proof system, which involves a new logical connective that allows changing the `frame of reference’—what corresponds in computer architectures to ‘‘virtual memory’’—and we argue that this proof system is complete with respect to a semantics that furthermore satisfies extensionality and comprehension.