• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Debugging
  • Projects
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
    • Kestrel-books
    • X86isa
      • Program-execution
      • Introduction
      • X86isa-build-instructions
      • Publications
      • Contributors
      • Machine
        • Syscalls
        • Cpuid
        • X86isa-state
        • Linear-memory
        • Rflag-specifications
        • Characterizing-undefined-behavior
        • Top-level-memory
        • App-view
          • Linear-memory-in-app-view
            • Rvm32
            • Rvm128
            • Canonical-address-p
            • Wvm32
            • Rvm80
            • Rvm64
            • Rvm48
            • Wvm80
            • Wvm64
            • Wvm48
            • Wvm128
            • Rvm16
            • Wvm16
            • Rvm08
            • Wvm08
        • X86-decoder
        • Physical-memory
        • Decoding-and-spec-utils
        • Instructions
        • X86-modes
        • Segmentation
        • Register-readers-and-writers
        • Other-non-deterministic-computations
        • Environment
        • Paging
      • Implemented-opcodes
      • Proof-utilities
      • To-do
      • Concrete-simulation-examples
      • Model-validation
      • Utils
      • Debugging-code-proofs
    • Execloader
    • Axe
  • Testing-utilities
  • Math

• 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

Rvm32

Rvm128

Canonical-address-p

Recognizer of a canonical address

Wvm32

Rvm80

Rvm64

Rvm48

Wvm80

Wvm64

Wvm48

Wvm128

Rvm16

Wvm16

Rvm08

Wvm08