Documentation

Miri.Input.CompilerNamedFields

Compiler-backed helpers.rs:280–312: libc array construction and named non-enum ADT field projection. Names come from compiler field declarations; neither offsets nor layout equality establish field/type identity.

source
def Miri.Input.CompilerNamedFields.fieldIndex (runtime : RuntimeMetadata) (parent : Interpreter.LocalLayout) (name : String) :
Except Interpreter.StepError Nat
Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def Miri.Input.CompilerNamedFields.libcArrayLayout {S : Type} (runtime : RuntimeMetadata) (arrays : RuntimeArrayQueries.Access S) (key : String) (count : UInt64) :
    EStateM Interpreter.StepError S Interpreter.LocalLayout
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def Miri.Input.CompilerNamedFields.iovecArrayLayout {S : Type} (runtime : RuntimeMetadata) (arrays : RuntimeArrayQueries.Access S) (count : UInt64) :
      EStateM Interpreter.StepError S Interpreter.LocalLayout
      Equations
      Instances For