From 263be25484b6df50e71702e46798881f1ccae5f6 Mon Sep 17 00:00:00 2001 From: Johnathan Van Why Date: Fri, 19 Mar 2021 09:27:36 -0700 Subject: [PATCH 1/3] Improvements to the README item on `-Zmiri-track-raw-pointers`. 1. The double quotes around are changed to backspaces, so will render correctly in markdown. 2. Clarify that -Zmiri-track-raw-pointers will never accept code that Miri would not have accepted without -Zmiri-track-raw-pointers. --- README.md | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/README.md b/README.md index ae70c80d5f0..59f7b970546 100644 --- a/README.md +++ b/README.md @@ -252,9 +252,10 @@ 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 "" occurring in the message -- this + can recognize false positives by `` occurring in the message -- this indicates a pointer that was cast from an integer, so Miri was unable to track - this pointer. + this pointer. It does not have false negatives; code that works with + `-Zmiri-track-raw-pointers` will work without `-Zmiri-track-raw-pointers`. Some native rustc `-Z` flags are also very relevant for Miri: From 03be4138ed134370979aec04ff5fe23cab6bcf74 Mon Sep 17 00:00:00 2001 From: Johnathan Van Why Date: Mon, 22 Mar 2021 15:35:18 -0700 Subject: [PATCH 2/3] `-Zmiri-track-raw-pointers` doc correction: it is not strictly more restrictive than Stacked Borrows. This change is based on the following comment: https://github.com/rust-lang/miri/pull/1748#issuecomment-803279473 --- README.md | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/README.md b/README.md index 59f7b970546..5e5b82b3654 100644 --- a/README.md +++ b/README.md @@ -254,8 +254,9 @@ environment variable: help identify latent aliasing issues in code that Miri accepts by default. You can recognize false positives by `` occurring in the message -- this indicates a pointer that was cast from an integer, so Miri was unable to track - this pointer. It does not have false negatives; code that works with - `-Zmiri-track-raw-pointers` will work without `-Zmiri-track-raw-pointers`. + 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`. Some native rustc `-Z` flags are also very relevant for Miri: From 12005612ab7f2c84d4ceca8132dd7483bd892061 Mon Sep 17 00:00:00 2001 From: Johnathan Van Why Date: Wed, 24 Mar 2021 16:20:54 -0700 Subject: [PATCH 3/3] README.md: Apply RalfJung's suggestion `-Zmiri-track-raw-pointers` isn't *much* more restrictive than normal Stacked Borrows. Co-authored-by: Ralf Jung --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index 5e5b82b3654..8a0c5180e00 100644 --- a/README.md +++ b/README.md @@ -256,7 +256,7 @@ environment variable: indicates a pointer that was cast from an integer, so Miri was unable to track 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`. + `-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: