| //@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/ |
| } |
| } |