Module miri::borrow_tracker::tree_borrows::perms::transition
source ยท Expand description
This module controls how each permission individually reacts to an access.
Although these functions take protected
as an argument, this is NOT because
we check protector violations here, but because some permissions behave differently
when protected.
Functionsยง
- child_
read ๐A child node was read-accessed: UB on Disabled, noop on the rest. - child_
write ๐A child node was write-accessed:Reserved
must becomeActive
to obtain write permissions,Frozen
andDisabled
cannot obtain such permissions and produce UB. - foreign_
read ๐A non-child node was read-accessed: keepReserved
but mark it asconflicted
if it is protected; invalidateActive
. - foreign_
write ๐A non-child node was write-accessed: this makes everythingDisabled
except for non-protected interior mutableReserved
which stay the same. - perform_
access ๐Dispatch handler depending on the kind of access and its position.