Source intrinsics.rs::ptr_offset_inbounds. Pointer resolution and live allocation metadata must be supplied by the machine's concrete memory state.

inductive Miri.Interpreter.PointerOffsetError : Type

• access (reason : Memory.AccessError) : PointerOffsetError
• pointer (reason : Memory.PointerError) : PointerOffsetError

@[instance_reducible]

instance Miri.Interpreter.instDecidableEqPointerOffsetError : DecidableEq PointerOffsetError

Equations

• Miri.Interpreter.instDecidableEqPointerOffsetError = Miri.Interpreter.instDecidableEqPointerOffsetError.decEq

def Miri.Interpreter.instDecidableEqPointerOffsetError.decEq (x✝ x✝¹ : PointerOffsetError) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Miri.Interpreter.instDecidableEqPointerOffsetError.decEq (Miri.Interpreter.PointerOffsetError.access reason) (Miri.Interpreter.PointerOffsetError.pointer reason_1) = isFalse ⋯
• Miri.Interpreter.instDecidableEqPointerOffsetError.decEq (Miri.Interpreter.PointerOffsetError.pointer reason) (Miri.Interpreter.PointerOffsetError.access reason_1) = isFalse ⋯

@[instance_reducible]

instance Miri.Interpreter.instReprPointerOffsetError : Repr PointerOffsetError

Equations

• Miri.Interpreter.instReprPointerOffsetError = { reprPrec := Miri.Interpreter.instReprPointerOffsetError.repr }

def Miri.Interpreter.instReprPointerOffsetError.repr : PointerOffsetError → Nat → Std.Format

Equations

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

def Miri.Interpreter.ptrOffsetInbounds {Prov ProvExtra : Type} (target : Memory.PointerArithmetic) (ptr : Memory.Pointer (Option Prov)) (offsetBytes : Int64) (resolve : Memory.PointerResolver Prov ProvExtra) (lookup : Memory.LiveAllocationLookup) : Except PointerOffsetError (Memory.Pointer (Option Prov))

Equations

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