A recent Rust PR tackled a Dafny-to-Rust soundness issue by making all references to self mutable. This had a lot of problematic implications, such as the impossibility to nest function calls, and in the future to have general traits.
This PR fixes the soundness issue with another way, to prevent the inlining of a function that otherwise Rust's global analysis might determine is safe to remove when it is not for Dafny.
How has this been tested?
A test that I checked was failing without the [inline(never)] annotation now succeeds.
Fixes #5774 and I added it as a test case as well.
By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.
Description
A recent Rust PR tackled a Dafny-to-Rust soundness issue by making all references to self mutable. This had a lot of problematic implications, such as the impossibility to nest function calls, and in the future to have general traits. This PR fixes the soundness issue with another way, to prevent the inlining of a function that otherwise Rust's global analysis might determine is safe to remove when it is not for Dafny.
How has this been tested?
A test that I checked was failing without the
[inline(never)]annotation now succeeds.Fixes #5774 and I added it as a test case as well.
By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.