Bind actual compiler libc value/signature evidence into the existing physical Unix memory and errno pipelines. Missing names remain unsupported; page-size, host errors, memory accesses and frame checks are runtime effects.

def Miri.Input.CompilerUnixMemoryQueries.ioErrorHooks {S Host : Type} (constants : CompilerNamedConstants.Prepared) (base : Interpreter.IoError.Hooks S Host) : Interpreter.IoError.Hooks S Host

Equations

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

def Miri.Input.CompilerUnixMemoryQueries.hooks {P S D MD B I : Type} (constants : CompilerNamedConstants.Prepared) (abis : CompilerNamedShimAbi.Prepared) (base : Interpreter.UnixMemory.Hooks P S D MD B I) : Interpreter.UnixMemory.Hooks P S D MD B I

Equations

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

def Miri.Input.CompilerUnixMemoryQueries.readOffset {P S : Type} [Memory.PointerProvenance P] (runtime : RuntimeMetadata) (readScalar : Interpreter.OpTy P → EStateM Interpreter.StepError S (Memory.Scalar P)) (operand : Interpreter.OpTy P) : EStateM Interpreter.StepError S Int

mmap offset conversion uses actual compiler libc::off_t size, independent of host width and pointer width. readScalar must be the real operand read.

Equations

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