Skip to content

Commit fd81880

Browse files
committed
Leave a trace of the current suboptimal status of foreign_write
1 parent 78f6386 commit fd81880

File tree

1 file changed

+6
-0
lines changed
  • src/tools/miri/src/borrow_tracker/tree_borrows

1 file changed

+6
-0
lines changed

src/tools/miri/src/borrow_tracker/tree_borrows/perms.rs

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -146,6 +146,12 @@ mod transition {
146146
/// non-protected interior mutable `Reserved` which stay the same.
147147
fn foreign_write(state: PermissionPriv, protected: bool) -> Option<PermissionPriv> {
148148
Some(match state {
149+
// FIXME: since the fix related to reservedim_spurious_write, it is now possible
150+
// to express these transitions of the state machine without an explicit dependency
151+
// on `protected`: because `ty_is_freeze: false` implies `!protected` then
152+
// the line handling `Reserved { .. } if protected` could be deleted.
153+
// This will however require optimizations to the exhaustive tests because
154+
// fewer initial conditions are valid.
149155
Reserved { .. } if protected => Disabled,
150156
res @ Reserved { ty_is_freeze: false, .. } => res,
151157
_ => Disabled,

0 commit comments

Comments
 (0)