As I understand it, Ada can't ensure that. The safe subset of Ada doesn't have allocation with multiple references. SPARK is mostly designed for things like avionics controllers, which tend not to allocate.