3 ms·
Stacked borrows is miri's runtime model. Run it under miri and you will see the error reported for the `*x = 10;` version but not the `write(x);` version - "Und
by Arnavion 1y ago
Stacked borrows is miri's runtime model. Run it under miri and you will see the error reported for the `*x = 10;` version but not the `write(x);` version - "Undefined Behavior: attempting a write access using [...] but that tag does not exist in the borrow stack for this location".
rustc itself has no reason to reject either version, because y is a *mut and thus has no borrow/lifetime relation to the &mut that x is, from a compile-time/typesystem perspective.
- vollbrecht 1y agoAh that make sense. Thanks for clarifying.
- haberman 1y agoThe paper mentions that the authors implemented tree borrows in Miri. Is this change likely to be adopted by Miri as the default model going forward?