• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Community
    • 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
          • App-view
            • Linear-memory-in-app-view
              • Canonical-address-p
              • Rvm512
              • Rvm32
              • Rvm256
              • Wvm32
              • Rvm128
              • Rvm80
              • Rvm64
              • Rvm48
              • Wvm512
              • Wvm64
              • Wvm48
              • Wvm256
              • Wvm128
              • Rvm16
              • Wvm80
              • Wvm16
              • Rvm08
              • Wvm08
          • Top-level-memory
          • 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
  • App-view

Linear-memory-in-app-view

Definition of linear memory accessor and updater functions, used when app-view = T

Note that the top-level memory accessor function is rml08 and updater function is wml08. Their 16, 32, and 64 bit counterparts are also available. These functions behave differently depending upon the value of app-view.

Subtopics

Canonical-address-p
Recognizer of a canonical address
Rvm512
Rvm32
Rvm256
Wvm32
Rvm128
Rvm80
Rvm64
Rvm48
Wvm512
Wvm64
Wvm48
Wvm256
Wvm128
Rvm16
Wvm80
Wvm16
Rvm08
Wvm08