Stateful application of the source freeze-sensitive visitor to a private map accumulator. Query effects remain in the caller's canonical state, while the source's private permission map is returned only after a complete visit.
def
Miri.TreeBorrows.FreezeMap.visit
{P S A : Type}
(h : FreezeVisitor.Hooks P S)
(budget : Nat)
(place : Interpreter.MPlaceTy P)
(size : ABI.Size)
(initial : A)
(action : Memory.AllocRange → Bool → EStateM Interpreter.StepError A Unit)
:
Execute actions in source visitor order. Query and earlier action effects survive a later failure; the private accumulator is not exposed as a successful map until the trailing frozen range has also been visited.
Equations
- One or more equations did not get rendered due to their size.