Skip to content

Commit 5a460a0

Browse files
committed
we correctly check that the perm is not lazy when triggering protectors
1 parent efc2af4 commit 5a460a0

File tree

1 file changed

+16
-0
lines changed

1 file changed

+16
-0
lines changed
Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
//@compile-flags: -Zmiri-tree-borrows
2+
3+
// Protectors should not trigger on uninitialized locations,
4+
// otherwise we can write safe code that triggers UB.
5+
// To test this we do a write access that disables a protected
6+
// location, but the location is actually outside of the protected range.
7+
8+
// Both x and y are protected here
9+
fn write_second(_x: &mut u8, y: &mut u8) {
10+
*y = 1;
11+
}
12+
13+
fn main() {
14+
let mut data = (0u8, 1u8);
15+
write_second(&mut data.0, &mut data.1);
16+
}

0 commit comments

Comments
 (0)