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
- A child node was read-accessed: UB on Disabled, noop on the rest.
- A child node was write-accessed:
Reserved
must becomeActive
to obtain write permissions,Frozen
andDisabled
cannot obtain such permissions and produce UB. - A non-child node was read-accessed: noop on non-protected Reserved, advance to Frozen otherwise.
- A non-child node was write-accessed: this makes everything
Disabled
except for non-protected interior mutableReserved
which stay the same. - Dispatch handler depending on the kind of access and its position.