aeneas icon indicating copy to clipboard operation
aeneas copied to clipboard

Bug: disjoint borrows in a slice

Open Nadrieril opened this issue 1 month ago • 0 comments
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.

Nadrieril avatar Oct 01 '25 09:10 Nadrieril