Exact libc eval_path_scalar constants. The original compiler row carries the full libc::<name> ValueNS path; this adapter requires that identity at the demand site before decoding the compiler value.

def Miri.Input.CompilerLibcConstants.scalar {P : Type} (prepared : CompilerNamedConstants.Prepared) (name : String) : Except String (Memory.Scalar P)

Equations

• Miri.Input.CompilerLibcConstants.scalar prepared name = do let _ ← Miri.Input.CompilerLibcConstants.exactRecord✝ prepared name Miri.Input.CompilerNamedConstants.scalar prepared name

def Miri.Input.CompilerLibcConstants.i32 (prepared : CompilerNamedConstants.Prepared) (name : String) : Except String Int32

Integer helpers preserve the canonical named-constant conversion after checking the exact source path, for source wrappers using eval_libc_i32.

Equations

• Miri.Input.CompilerLibcConstants.i32 prepared name = do let _ ← Miri.Input.CompilerLibcConstants.exactRecord✝ prepared name Miri.Input.CompilerNamedConstants.i32 prepared name