Pinned windows/foreign_items.rs::win_get_full_path_name and its shim arm. Unix-host normalization deliberately retains the upstream approximation.

@[reducible, inline]

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

Equations

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

inductive Miri.Interpreter.WindowsPaths.Normalized : Type

• direct (bytes : ByteArray) : Normalized
• absolute (bytes : ByteArray) : Normalized

def Miri.Interpreter.WindowsPaths.normalizeUnix (bytes : ByteArray) : Normalized

Equations

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

structure Miri.Interpreter.WindowsPaths.Hooks (S F H D Path HM Time E Kind : Type) : Type

• files : WindowsFiles.Hooks S F H D Path HM Time E
• strings : OsStrings.Hooks Memory.Provenance S Path Kind
• absolute : Path → M S (Except (IoError.HostError E) Path)

def Miri.Interpreter.WindowsPaths.fullPath {S F H D P HM T E K : Type} (h : Hooks S F H D P HM T E K) (path : P) : M S (Except (IoError.HostError E) P)

Equations

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

def Miri.Interpreter.WindowsPaths.getFullPath {S F H D P HM T E K : Type} (h : Hooks S F H D P HM T E K) (name size buffer filepart : OpTy Memory.Provenance) : M S UInt32

Equations

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