Actual std-only mmap policy consumes the source frame predicate.

def Miri.Interpreter.FrameMetadataBindings.unixMemory {K User D MD B I : Type} (compiler : FrameMetadata.CompilerHooks K User) (base : UnixMemory.Hooks Memory.Provenance (MachineHooks.State K User) D MD B I) : UnixMemory.Hooks Memory.Provenance (MachineHooks.State K User) D MD B I

Equations

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