Remaining pinned windows/env.rs host-path operations. Windows environment storage and buffer-size policy reuse EnvVars rather than another environment.

@[reducible, inline]

abbrev Miri.Interpreter.WindowsEnvironment.M (σ α : Type) : Type

Equations

• Miri.Interpreter.WindowsEnvironment.M = EStateM Miri.Interpreter.StepError

structure Miri.Interpreter.WindowsEnvironment.Hooks (S Os E Kind : Type) : Type

• env : EnvVars.Hooks (Option Memory.Provenance) Os S
• strings : OsStrings.Hooks Memory.Provenance S Os Kind
• process : EnvVars.ProcessHooks S
• errors : IoError.Hooks S E
• readU32 : OpTy Memory.Provenance → M S UInt32
• readPointer : OpTy Memory.Provenance → M S (Memory.Pointer (Option Memory.Provenance))
• readIsize : OpTy Memory.Provenance → M S Int
• readPlaceU32 : MPlaceTy Memory.Provenance → M S UInt32
• derefU32 : OpTy Memory.Provenance → M S (MPlaceTy Memory.Provenance)
• writeU32 : UInt32 → MPlaceTy Memory.Provenance → M S Unit
• isolationReject : String → M S Bool
• checkNoIsolation : String → M S Unit
• currentDirectory : M S (Except (IoError.HostError E) Os)
• setCurrentDirectory : Os → M S (Except (IoError.HostError E) Unit)
• userHomeDirectory : M S (Option Os)
• temporaryDirectory : M S Os
• windows : String → M S (Memory.Scalar Memory.Provenance)

def Miri.Interpreter.WindowsEnvironment.getcwd {S O E K : Type} (h : Hooks S O E K) (size buf : OpTy Memory.Provenance) : M S UInt32

Equations

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

def Miri.Interpreter.WindowsEnvironment.chdir {S O E K : Type} (h : Hooks S O E K) (path : OpTy Memory.Provenance) : M S (Memory.Scalar Memory.Provenance)

Equations

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

def Miri.Interpreter.WindowsEnvironment.profile {S O E K : Type} (h : Hooks S O E K) (token buf size : OpTy Memory.Provenance) : M S Bool

Equations

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

def Miri.Interpreter.WindowsEnvironment.tempPath {S O E K : Type} (h : Hooks S O E K) (length buf : OpTy Memory.Provenance) : M S UInt32

Equations

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