@@ -22,6 +22,11 @@ enum PermissionPriv {
2222 /// - foreign-read then child-write is UB due to `conflicted`,
2323 /// - child-write then foreign-read is UB since child-write will activate and then
2424 /// foreign-read disables a protected `Active`, which is UB.
25+ ///
26+ /// Note: since the discovery of `tests/fail/tree_borrows/reservedim_spurious_write.rs`,
27+ /// `ty_is_freeze` does not strictly mean that the type has no interior mutability,
28+ /// it could be an interior mutable type that lost its interior mutability privileges
29+ /// when retagged with a protector.
2530 Reserved { ty_is_freeze : bool , conflicted : bool } ,
2631 /// represents: a unique pointer;
2732 /// allows: child reads, child writes;
@@ -141,6 +146,12 @@ mod transition {
141146 /// non-protected interior mutable `Reserved` which stay the same.
142147 fn foreign_write ( state : PermissionPriv , protected : bool ) -> Option < PermissionPriv > {
143148 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.
144155 Reserved { .. } if protected => Disabled ,
145156 res @ Reserved { ty_is_freeze : false , .. } => res,
146157 _ => Disabled ,
0 commit comments