Borrowing Safe Pointers from Rust in SPARK

In the field of deductive software verification, programs with pointers present a major challenge due to pointer aliasing.