aeneas
aeneas copied to clipboard
Bug: disjoint borrows in a slice
trafficstars
This is valid Rust code:
fn disjoint_borrows_in_slice() {
struct Test {
a: i32,
b: i32,
}
let inputs: &mut [_] = &mut [Test { a: 0, b: 0 }];
let a = &mut inputs[0].a;
let b = &mut inputs[0].b;
*a = 0;
*b = 1;
}
Aeneas can't support this today because we pretend that slice indexing is done through a function call. Rust actually considers indexing slices/arrays to be a built-in projection and therefore considers these borrows disjoint.