Direct memory-access capability construction. Compiler globals use the actual lazy conversion and global-specific extra initialization. Byte backing, root addressing, external-allocation access and diagnostic retention remain real source capabilities; memory effects use the canonical machine. Sources: machine.rs before_memory_read/write; memory.rs get_alloc_raw.

@[reducible, inline]

abbrev Miri.Input.EvalAccessMachine.User (Os R P H D O Aff B Host : Type) : Type

Equations

• Miri.Input.EvalAccessMachine.User = Miri.Input.EvalCoreMachine.User

@[reducible, inline]

abbrev Miri.Input.EvalAccessMachine.State (Os R P H D O Aff B Host : Type) : Type

Equations

• Miri.Input.EvalAccessMachine.State = Miri.Input.EvalCoreMachine.State

def Miri.Input.EvalAccessMachine.make {Os R P H D O Aff B Host : Type} (p : CompilerProviders.Prepared) (image : AllocationImage.Imported) (maximum : ABI.Size) (fuel : Nat) (globals : Memory.GlobalAllocationHooks Memory.Provenance TreeBorrows.BorrowTree Memory.MiriMemoryKind (Interpreter.PlaceMachine.AccessState Memory.MiriMemoryKind (User Os R P H D O Aff B Host))) (pointers : Interpreter.PointerMachine.Hooks Memory.MiriMemoryKind (Interpreter.ValidityMachine.Control (EvalCoreMachine.Stored Os R P H D O Aff B Host))) (extras : Interpreter.MemoryExtras.Hooks Memory.MiriMemoryKind (User Os R P H D O Aff B Host) P) : Interpreter.PlaceMachine.AccessConfig Memory.MiriMemoryKind (User Os R P H D O Aff B Host)

Equations

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