Documentation

Miri.Interpreter.ArrayProjection

Pinned interpret/projection.rs project_array_fields / ArrayIterator for memory places. The endpoint probe and element-layout query happen once before iteration; each subsequent projection uses the cached source layout.

source
@[reducible, inline]
abbrev Miri.Interpreter.ArrayProjection.M (σ α : Type) :
Type
Equations
Instances For
    source
    structure Miri.Interpreter.ArrayProjection.Iterator :
    Type
    Instances For
      source
      def Miri.Interpreter.ArrayProjection.prepare {S C E : Type} (h : PlaceProjectionHooks Memory.Provenance S C E) (choice : C) (unitLayout : M S LocalLayout) (base : MPlaceTy Memory.Provenance) :
      M S Iterator
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def Miri.Interpreter.ArrayProjection.get {S C E : Type} (h : PlaceProjectionHooks Memory.Provenance S C E) (choice : C) (iterator : Iterator) (index : Nat) :
        M S (MPlaceTy Memory.Provenance)
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For