Auto merge of #1748 - jrvanwhy:track-raw-pointers-doc, r=RalfJung
Improvements to the README item on `-Zmiri-track-raw-pointers`. [Rendered](https://github.com/jrvanwhy/miri/tree/track-raw-pointers-doc) 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`.
This commit is contained in:
commit
91aeb04408
@ -252,9 +252,11 @@ environment variable:
|
||||
* `-Zmiri-track-raw-pointers` makes Stacked Borrows track a pointer tag even for
|
||||
raw pointers. This can make valid code fail to pass the checks, but also can
|
||||
help identify latent aliasing issues in code that Miri accepts by default. You
|
||||
can recognize false positives by "<untagged>" occurring in the message -- this
|
||||
can recognize false positives by `<untagged>` occurring in the message -- this
|
||||
indicates a pointer that was cast from an integer, so Miri was unable to track
|
||||
this pointer.
|
||||
this pointer. Note that it is not currently guaranteed that code that works
|
||||
with `-Zmiri-track-raw-pointers` also works without
|
||||
`-Zmiri-track-raw-pointers`, but for the vast majority of code, this will be the case.
|
||||
|
||||
Some native rustc `-Z` flags are also very relevant for Miri:
|
||||
|
||||
|
Loading…
Reference in New Issue
Block a user