Documentation

Miri.Interpreter.LeakCheck

rustc interpret/memory.rs::take_leaked_allocations. This is deliberately separate from provenance GC: only global-kind allocations and static_roots seed leak reachability. Taking leaks is destructive and permits no continuation.

source
def Miri.Interpreter.LeakCheck.allocationIds {E : Type} (allocation : Memory.Allocation Memory.Provenance E) :
Array Memory.AllocId
Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def Miri.Interpreter.LeakCheck.mayLeak :
    Memory.MemoryKind Memory.MiriMemoryKind → Bool
    Equations
    Instances For
      source
      def Miri.Interpreter.LeakCheck.takeProfiled {E : Type} (profile : Lean.Options) (memory : Memory.MemoryState Memory.Provenance E Memory.MiriMemoryKind) (staticRoots : Array Memory.AllocId) :
      Except StepError (Memory.MemoryState Memory.Provenance E Memory.MiriMemoryKind × Array (Memory.AllocId × Memory.LocalAllocation Memory.Provenance E Memory.MiriMemoryKind))

      No access/retag/deallocation hook runs here. Source removes allocations straight from alloc_map after reachability, retaining their bytes and extras in the returned report. Missing unchanged compiler globals do not add edges.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def Miri.Interpreter.LeakCheck.take {E : Type} (memory : Memory.MemoryState Memory.Provenance E Memory.MiriMemoryKind) (staticRoots : Array Memory.AllocId) :
        Except StepError (Memory.MemoryState Memory.Provenance E Memory.MiriMemoryKind × Array (Memory.AllocId × Memory.LocalAllocation Memory.Provenance E Memory.MiriMemoryKind))
        Equations
        Instances For
          source
          theorem Miri.Interpreter.LeakCheck.takeProfiled_eq_take {E : Type} (profile : Lean.Options) (memory : Memory.MemoryState Memory.Provenance E Memory.MiriMemoryKind) (staticRoots : Array Memory.AllocId) :
          takeProfiled profile memory staticRoots = take memory staticRoots