mikros/rust
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Leave a trace of the current suboptimal status of foreign_write

Browse Source
This commit is contained in:
Neven Villani 2024-07-12 15:58:59 +02:00
parent 78f6386b62
commit fd81880c91
No known key found for this signature in database
GPG Key ID: 00E765FA7F4F2EDE
1 changed files with 6 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
src/tools/miri/src/borrow_tracker/tree_borrows/perms.rs
View File

@ -146,6 +146,12 @@ mod transition {
/// non-protected interior mutable `Reserved` which stay the same.
fn foreign_write(state: PermissionPriv, protected: bool) -> Option<PermissionPriv> {
Some(match state {
// FIXME: since the fix related to reservedim_spurious_write, it is now possible
// to express these transitions of the state machine without an explicit dependency
// on `protected`: because `ty_is_freeze: false` implies `!protected` then
// the line handling `Reserved { .. } if protected` could be deleted.
// This will however require optimizations to the exhaustive tests because
// fewer initial conditions are valid.
Reserved { .. } if protected => Disabled,
res @ Reserved { ty_is_freeze: false, .. } => res,
_ => Disabled,