Stacked Borrows In Kani -- Extend Feature to handle more code

[jsalzbergedu]

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.

[jsalzbergedu]

We also need to overcome the following limitations:

• Model malloc,
• Model pointer manipulation,
• Model two phase borrows,
• Model function calls and closures.

[jsalzbergedu]

The stacked borrows model also currently does not handle function contracts; if relational data is checked in the pre and post conditions, then because we only check one byte currently, there is no way to check it. Many function contracts however may work, and so testing will need to confirm these boundaries.

Also it should be possible to disable demonic nondeterminism, and it isn't currently.