Exact current-state rendering used by Tree Borrows' print_tree diagnostic. Diagnostic histories are intentionally absent because this source printer renders current node names, permissions, protectors and exposure only.

structure Miri.TreeBorrows.DiagnosticsRender.Node : Type

• tag : Memory.BorTag
• name : Option String
• exposed : Bool
• permissions : Array (Option Tree.LocationState)
• children : Array Node

partial def Miri.TreeBorrows.DiagnosticsRender.extractForest (tree : BorrowTree) (index : UniIndex) (ranges : Array (DataStructures.RangeMapSegment LocationTree)) (showUnnamed : Bool) : Except String (Array Node)

partial def Miri.TreeBorrows.DiagnosticsRender.nodeLines (node : Node) (padding : Array Nat) (tags : ProtectedTags) (indent : String) (lastChild wildcardRoot : Bool) : Array String

def Miri.TreeBorrows.DiagnosticsRender.render (tree : BorrowTree) (protectedTags : ProtectedTags) (showUnnamed : Bool) : Except String (Array String)

Produce the exact lines emitted by pinned Tree::print_tree; the caller uses stderr write_all and ignores returned host I/O errors as upstream does.

Equations

• One or more equations did not get rendered due to their size.