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.


  • 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 become Active to obtain write permissions, Frozen and Disabled cannot obtain such permissions and produce UB.
  • foreign_read ๐Ÿ”’
    A non-child node was read-accessed: keep Reserved but mark it as conflicted if it is protected; invalidate Active.
  • foreign_write ๐Ÿ”’
    A non-child node was write-accessed: this makes everything Disabled except for non-protected interior mutable Reserved which stay the same.
  • perform_access ๐Ÿ”’
    Dispatch handler depending on the kind of access and its position.