• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
      • Kestrel-books
      • X86isa
        • Program-execution
        • Sdm-instruction-set-summary
        • Tlb
        • Running-linux
        • Introduction
        • Asmtest
        • X86isa-build-instructions
        • Publications
        • Contributors
        • Machine
          • X86isa-state
          • Syscalls
          • Cpuid
          • Linear-memory
          • Rflag-specifications
          • Characterizing-undefined-behavior
          • Top-level-memory
            • Rme32
            • Rime32
            • Gen-read-function
            • Rme256
            • Rme128
            • Rime64
            • Rime16
            • Rme80
            • Rme64
            • Rme48
            • Rme16
            • Gen-write-function
            • Rme-size
            • Rme08
            • Rime08
            • Rime-size
            • Wme-size
            • Wime-size
            • Wme32
            • Wime32
            • Wme80
            • Wme64
            • Wme48
            • Wme256
            • Wme16
            • Wme128
            • Wime64
            • Wime16
            • Address-aligned-p
            • Wme08
            • Wime08
          • App-view
          • X86-decoder
          • Physical-memory
          • Decoding-and-spec-utils
          • Instructions
          • Register-readers-and-writers
          • X86-modes
          • Segmentation
          • Other-non-deterministic-computations
          • Environment
          • Paging
        • Implemented-opcodes
        • To-do
        • Proof-utilities
        • Peripherals
        • Model-validation
        • Modelcalls
        • Concrete-simulation-examples
        • Utils
        • Debugging-code-proofs
      • Axe
      • Execloader
    • Math
    • Testing-utilities
  • Machine

Top-level-memory

Top-level Memory Accessor and Updater Functions

Subtopics

Rme32
Read an unsigned 32-bit value from memory via an effective address.
Rime32
Read a signed 32-bit value from memory via an effective address.
Gen-read-function
Rme256
Read an unsigned 256-bit value from memory via an effective address.
Rme128
Read an unsigned 128-bit value from memory via an effective address.
Rime64
Read a signed 64-bit value from memory via an effective address.
Rime16
Read a signed 16-bit value from memory via an effective address.
Rme80
Read an unsigned 80-bit value from memory via an effective address.
Rme64
Read an unsigned 64-bit value from memory via an effective address.
Rme48
Read an unsigned 48-bit value from memory via an effective address.
Rme16
Read an unsigned 16-bit value from memory via an effective address.
Gen-write-function
Rme-size
Read an unsigned value with the specified number of bytes from memory via an effective address.
Rme08
Read an unsigned 8-bit value from memory via an effective address.
Rime08
Read a signed 8-bit value from memory via an effective address.
Rime-size
Read a signed value with the specified number of bytes from memory via an effective address.
Wme-size
Write an unsigned value with the specified number of bytes to memory via an effective address.
Wime-size
Write a signed value with the specified number of bytes to memory via an effective address.
Wme32
Write an unsigned 32-bit value to memory via an effective address.
Wime32
Write a signed 32-bit value to memory via an effective address.
Wme80
Write an unsigned 80-bit value to memory via an effective address.
Wme64
Write an unsigned 64-bit value to memory via an effective address.
Wme48
Write an unsigned 48-bit value to memory via an effective address.
Wme256
Write an unsigned 256-bit value to memory via an effective address.
Wme16
Write an unsigned 16-bit value to memory via an effective address.
Wme128
Write an unsigned 128-bit value to memory via an effective address.
Wime64
Write a signed 64-bit value to memory via an effective address.
Wime16
Write a signed 16-bit value to memory via an effective address.
Address-aligned-p
Check the alignment of a linear address.
Wme08
Write an unsigned 8-bit value to memory via an effective address.
Wime08
Write a signed 8-bit value to memory via an effective address.