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:
- We need to add regression tests for and implement the following syntactic constructs:
- Function calls
- Moving pointers
- Copying pointers
- 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.
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:
And we ought to see if Kani can find aliasing model violations in codebases that MIRI has not yet.