diff --git a/tests/compile-fail/stacked_borrows/raw_tracking.rs b/tests/compile-fail/stacked_borrows/raw_tracking.rs new file mode 100644 index 000000000000..b9ddee328f7a --- /dev/null +++ b/tests/compile-fail/stacked_borrows/raw_tracking.rs @@ -0,0 +1,13 @@ +// compile-flags: -Zmiri-track-raw-pointers +// ignore-windows (FIXME: tracking raw pointers does not work on Windows) +//! This demonstrates a provenance problem that requires tracking of raw pointers to be detected. + +fn main() { + let mut l = 13; + let raw1 = &mut l as *mut _; + let raw2 = &mut l as *mut _; // invalidates raw1 + // Without raw pointer tracking, Stacked Borrows cannot distinguish raw1 and raw2, and thus + // fails to realize that raw1 should not be used any more. + unsafe { *raw1 = 13; } //~ ERROR no item granting write access to tag + unsafe { *raw2 = 13; } +} diff --git a/tests/run-pass/format.rs b/tests/run-pass/format.rs index 3893efcb26a1..053cce36130c 100644 --- a/tests/run-pass/format.rs +++ b/tests/run-pass/format.rs @@ -1,5 +1,3 @@ -// compile-flags: -Zmiri-track-raw-pointers - fn main() { println!("Hello {}", 13); println!("{:0(dummy: &mut T, iter: impl Iterator) { diff --git a/tests/run-pass/vecdeque.rs b/tests/run-pass/vecdeque.rs index 54aeb89ec83f..55b47f622fde 100644 --- a/tests/run-pass/vecdeque.rs +++ b/tests/run-pass/vecdeque.rs @@ -1,4 +1,5 @@ // compile-flags: -Zmiri-track-raw-pointers +// ignore-windows (FIXME: tracking raw pointers does not work on Windows) use std::collections::VecDeque; fn test_all_refs<'a, T: 'a>(dummy: &mut T, iter: impl Iterator) {