| //@compile-flags: -Zmiri-tree-borrows | |
| use core::ptr::addr_of_mut; | |
| // Check that the diagnostics correctly report the exact range at fault | |
| // and trim irrelevant events. | |
| fn main() { | |
| unsafe { | |
| let data = &mut [0u8; 16]; | |
| // Create and activate a few bytes | |
| let rmut = &mut *addr_of_mut!(data[0..6]); | |
| rmut[3] += 1; | |
| rmut[4] += 1; | |
| rmut[5] += 1; | |
| // Now make them lose some perms | |
| let _v = data[3]; | |
| let _v = data[4]; | |
| let _v = data[5]; | |
| data[4] = 1; | |
| data[5] = 1; | |
| // Final test | |
| rmut[5] += 1; //~ ERROR: /read access through .* is forbidden/ | |
| } | |
| } |