blob: fee88cf3486afe29aab868a4f1b087adf4306ee8 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
|
//@compile-flags: -Zmiri-tree-borrows
// Check that TB properly rejects alternating Reads and Writes, but tolerates
// alternating only Reads to Reserved mutable references.
pub fn main() {
let x = &mut 0u8;
let y = unsafe { &mut *(x as *mut u8) };
// Foreign Read, but this is a no-op from the point of view of y (still Reserved)
let _val = *x;
// Now we activate y, for this to succeed y needs to not have been Frozen
// by the previous operation
*y += 1; // Success
// This time y gets Frozen...
let _val = *x;
// ... and the next Write attempt fails.
//~v ERROR: /write access through .* is forbidden/
*y += 1; // Failure
let _val = *x;
*y += 1; // Unreachable
}
|
