Closed Saecki closed 3 weeks ago
This is not a false positive. The ranges printed by the diagnostics are exclusive on the end, like Rust ranges. 0..5
does not include 5.
Alternatively if you mean you think that Stacked Borrows should be changed to accept this code, that's part of what Tree Borrows is for. Set MIRIFLAGS=-Zmiri-tree-borrows
to use that model instead. Your code is trying to do the &Header pattern: https://github.com/rust-lang/unsafe-code-guidelines/issues/256
I'm closing this because it is not a bug in Miri (which essentially does not have false positives), but I don't want to discourage you from asking further questions about this situation or diagnostic.
The code above fails with the following message:
Is the unsafe code not quite right, or is this a false positive?