Documentation

Miri.Memory.AllocRange

Checked byte ranges used by the rustc allocation interpreter.

source
inductive Miri.Memory.MemoryError :
Type

Failures that upstream represents as a checked-size error or a panic.

Instances For
    source
    def Miri.Memory.instDecidableEqMemoryError.decEq (x✝ x✝¹ : MemoryError) :
    Decidable (x✝ = x✝¹)
    Equations
    Instances For
      source
      @[instance_reducible]
      instance Miri.Memory.instDecidableEqMemoryError :
      DecidableEq MemoryError
      Equations
      source
      def Miri.Memory.instReprMemoryError.repr :
      MemoryError → Nat → Std.Format
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[instance_reducible]
        instance Miri.Memory.instReprMemoryError :
        Repr MemoryError
        Equations
        source
        @[instance_reducible]
        instance Miri.Memory.instToStringMemoryError :
        ToString MemoryError
        Equations
        • One or more equations did not get rendered due to their size.
        source
        structure Miri.Memory.AllocRange :
        Type

        An access interval represented by start offset and byte length.

        Instances For
          source
          @[instance_reducible]
          instance Miri.Memory.instDecidableEqAllocRange :
          DecidableEq AllocRange
          Equations
          source
          def Miri.Memory.instDecidableEqAllocRange.decEq (x✝ x✝¹ : AllocRange) :
          Decidable (x✝ = x✝¹)
          Equations
          Instances For
            source
            def Miri.Memory.instReprAllocRange.repr :
            AllocRange → Nat → Std.Format
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              @[instance_reducible]
              instance Miri.Memory.instReprAllocRange :
              Repr AllocRange
              Equations
              source
              def Miri.Memory.allocRange (start size : ABI.Size) :
              AllocRange

              Construct an access range from its start and byte size.

              Equations
              Instances For
                source
                def Miri.Memory.AllocRange.end (range : AllocRange) :
                Except MemoryError ABI.Size

                Checked exclusive end offset, mirroring AllocRange::end and Size addition.

                Equations
                Instances For
                  source
                  def Miri.Memory.AllocRange.endExclusive (range : AllocRange) :
                  Except MemoryError ABI.Size

                  Descriptive alias for the checked exclusive end offset.

                  Equations
                  Instances For
                    source
                    def Miri.Memory.AllocRange.fromEndpoints (start finish : ABI.Size) :
                    Except MemoryError AllocRange

                    Checked construction from two endpoints, mirroring Size subtraction.

                    Equations
                    Instances For
                      source
                      def Miri.Memory.AllocRange.subrange (range subrange : AllocRange) :
                      Except MemoryError AllocRange

                      Return a subrange relative to this interval or report the source assertion failure.

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