move
move copied to clipboard
[move-prover][interpreter] two bug fixes to re-enable disabled tests
The first commit fixes two bugs to re-enable the failing test:
- collect pointers for write-backs even when the local slot is destroyed
- fix the indexing of the borrow edge in the write-back process.
The second commit picks the baseline
version for callee with ghost type params
- This is a temporary solution until we have a better way to multiplex the spec evaluation against multiple universially quantified types.
Motivation
As title
Have you read the Contributing Guidelines on pull requests?
Yes
Test Plan
CI, with the re-enabled test.