Improvements to the README item on -Zmiri-track-raw-pointers.

[jrvanwhy]

Rendered

Minor change: I changed the quotes around <untagged> into backticks, so they render correctly in markdown.

Significant change: I documented that -Zmiri-track-raw-pointers is a strictly more restrictive model that "normal" Stacked Borrows. I am not confident this change is correct, please verify it. If this change is not correct, let me know, and I'll update this PR to document that :-)

EDIT: I was wrong, -Zmiri-track-raw-pointers may not be strictly more restrictive. I added the following sentence to prevent others from making the same assumption that I did:

Note that it is not currently guaranteed that code that works with -Zmiri-track-raw-pointers also works without -Zmiri-track-raw-pointers.

[RalfJung]

Thanks for the PR!

I documented that -Zmiri-track-raw-pointers is a strictly more restrictive model that "normal" Stacked Borrows. I am not confident this change is correct, please verify it.

I wish this was true, but I am slightly worried that due to rust-lang/unsafe-code-guidelines#273, this might not actually be true...

[jrvanwhy]

I documented that -Zmiri-track-raw-pointers is a strictly more restrictive model that "normal" Stacked Borrows. I am not confident this change is correct, please verify it.

I wish this was true, but I am slightly worried that due to rust-lang/unsafe-code-guidelines#273, this might not actually be true...

Okay, I replaced the sentence with one that makes it clear it may not be strictly more restrictive. Let me know if you'd like me to squash the commits together, or to add a link to your comment to the README entry.

[jrvanwhy]

Thanks for the PR!

I documented that -Zmiri-track-raw-pointers is a strictly more restrictive model that "normal" Stacked Borrows. I am not confident this change is correct, please verify it.

I wish this was true, but I am slightly worried that due to rust-lang/unsafe-code-guidelines#273, this might not actually be true...

I have verified that the code in that example runs fine with -Zmiri-track-raw-pointers but Miri detects undefined behavior without -Zmiri-track-raw-pointers, so unfortunately your concern is correct.

[RalfJung]

I have verified that the code in that example runs fine with -Zmiri-track-raw-pointers but Miri detects undefined behavior without -Zmiri-track-raw-pointers, so unfortunately your concern is correct.

FWIW, note that it is not entirely clear which of the two answers is even correct here. We probably don't want this code to be UB.

[RalfJung]

Thanks for improving our docs. :)
@bors r+

[bors]

📌 Commit 1200561 has been approved by RalfJung

[bors]

⌛ Testing commit 1200561 with merge 91aeb04...

[bors]

☀️ Test successful - checks-actions
Approved by: RalfJung
Pushing 91aeb04 to master...