@@ -22,6 +22,11 @@ enum PermissionPriv {
22
22
/// - foreign-read then child-write is UB due to `conflicted`,
23
23
/// - child-write then foreign-read is UB since child-write will activate and then
24
24
/// 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.
25
30
Reserved { ty_is_freeze : bool , conflicted : bool } ,
26
31
/// represents: a unique pointer;
27
32
/// allows: child reads, child writes;
@@ -141,6 +146,12 @@ mod transition {
141
146
/// non-protected interior mutable `Reserved` which stay the same.
142
147
fn foreign_write ( state : PermissionPriv , protected : bool ) -> Option < PermissionPriv > {
143
148
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.
144
155
Reserved { .. } if protected => Disabled ,
145
156
res @ Reserved { ty_is_freeze : false , .. } => res,
146
157
_ => Disabled ,
0 commit comments