Exact Miri machine allocation kinds and leak policy from the pinned machine.rs. Leak permission classifies allocation ownership; it is not a claim that an access is valid or a program is UB-free.

inductive Miri.Memory.MiriMemoryKind : Type

• rust : MiriMemoryKind
• miri : MiriMemoryKind
• c : MiriMemoryKind
• winHeap : MiriMemoryKind
• winLocal : MiriMemoryKind
• machine : MiriMemoryKind
• runtime : MiriMemoryKind
• global : MiriMemoryKind
• externStatic : MiriMemoryKind
• tls : MiriMemoryKind
• mmap : MiriMemoryKind
• socketAddress : MiriMemoryKind

@[instance_reducible]

instance Miri.Memory.instDecidableEqMiriMemoryKind : DecidableEq MiriMemoryKind

Equations

• Miri.Memory.instDecidableEqMiriMemoryKind x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Miri.Memory.instReprMiriMemoryKind : Repr MiriMemoryKind

Equations

• Miri.Memory.instReprMiriMemoryKind = { reprPrec := Miri.Memory.instReprMiriMemoryKind.repr }

def Miri.Memory.instReprMiriMemoryKind.repr : MiriMemoryKind → Nat → Std.Format

Equations

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

def Miri.Memory.MiriMemoryKind.mayLeak : MiriMemoryKind → Bool

Equations

• Miri.Memory.MiriMemoryKind.rust.mayLeak = false
• Miri.Memory.MiriMemoryKind.miri.mayLeak = false
• Miri.Memory.MiriMemoryKind.c.mayLeak = false
• Miri.Memory.MiriMemoryKind.winHeap.mayLeak = false
• Miri.Memory.MiriMemoryKind.winLocal.mayLeak = false
• Miri.Memory.MiriMemoryKind.runtime.mayLeak = false
• Miri.Memory.MiriMemoryKind.machine.mayLeak = true
• Miri.Memory.MiriMemoryKind.global.mayLeak = true
• Miri.Memory.MiriMemoryKind.externStatic.mayLeak = true
• Miri.Memory.MiriMemoryKind.tls.mayLeak = true
• Miri.Memory.MiriMemoryKind.mmap.mayLeak = true
• Miri.Memory.MiriMemoryKind.socketAddress.mayLeak = true

def Miri.Memory.MiriMemoryKind.shouldSaveAllocationSpan : MiriMemoryKind → Bool

Source allocation-span selection, retained independently of leak policy.

Equations

• Miri.Memory.MiriMemoryKind.rust.shouldSaveAllocationSpan = true
• Miri.Memory.MiriMemoryKind.miri.shouldSaveAllocationSpan = true
• Miri.Memory.MiriMemoryKind.c.shouldSaveAllocationSpan = true
• Miri.Memory.MiriMemoryKind.winHeap.shouldSaveAllocationSpan = true
• Miri.Memory.MiriMemoryKind.winLocal.shouldSaveAllocationSpan = true
• Miri.Memory.MiriMemoryKind.mmap.shouldSaveAllocationSpan = true
• Miri.Memory.MiriMemoryKind.machine.shouldSaveAllocationSpan = false
• Miri.Memory.MiriMemoryKind.global.shouldSaveAllocationSpan = false
• Miri.Memory.MiriMemoryKind.externStatic.shouldSaveAllocationSpan = false
• Miri.Memory.MiriMemoryKind.tls.shouldSaveAllocationSpan = false
• Miri.Memory.MiriMemoryKind.runtime.shouldSaveAllocationSpan = false
• Miri.Memory.MiriMemoryKind.socketAddress.shouldSaveAllocationSpan = false