Currently, Stacked Borrows is implemented in the feature branch features/stacked_borrows.
However, to merge it into the main code-base, the following updates are needed:

1. We need to add regression tests for and implement the following syntactic constructs:

• Function calls
• Moving pointers
• Copying pointers

2. We need to have an extensive suite of regression tests, including

• Tests on the standard library
• Some of MIRI's regression tests
• Complex tests of our own design

And we ought to see if Kani can find aliasing model violations in codebases that MIRI has not yet.