From fd81880c9108c4b98839d55fe29884a625f05f02 Mon Sep 17 00:00:00 2001 From: Neven Villani Date: Fri, 12 Jul 2024 15:58:59 +0200 Subject: [PATCH] Leave a trace of the current suboptimal status of foreign_write --- src/tools/miri/src/borrow_tracker/tree_borrows/perms.rs | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/src/tools/miri/src/borrow_tracker/tree_borrows/perms.rs b/src/tools/miri/src/borrow_tracker/tree_borrows/perms.rs index 9c19ae76a2d..8e23257b6c0 100644 --- a/src/tools/miri/src/borrow_tracker/tree_borrows/perms.rs +++ b/src/tools/miri/src/borrow_tracker/tree_borrows/perms.rs @@ -146,6 +146,12 @@ mod transition { /// non-protected interior mutable `Reserved` which stay the same. fn foreign_write(state: PermissionPriv, protected: bool) -> Option { 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,