		Search-engine friendly clone of the ACL2 documentation.

Linear-memory

Rml-size

Signature
(rml-size nbytes addr r-x x86) → (mv * * x86)

Definitions and Theorems

Function: rml-size$inline

(defun rml-size$inline (nbytes addr r-x x86)
  (declare (xargs :stobjs (x86)))
  (declare (type (member 1 2 4 6 8 10 16 32)
                 nbytes)
           (type (signed-byte 48) addr)
           (type (member :r :x) r-x))
  (declare (xargs :guard (natp nbytes)))
  (case nbytes
    (1 (rml08 addr r-x x86))
    (2 (rml16 addr r-x x86))
    (4 (rml32 addr r-x x86))
    (6 (rml48 addr r-x x86))
    (8 (rml64 addr r-x x86))
    (10 (rml80 addr r-x x86))
    (16 (rml128 addr r-x x86))
    (32 (rml256 addr r-x x86))
    (otherwise
         (if (mbe :logic (canonical-address-p (+ -1 nbytes addr))
                  :exec (< (+ -1 nbytes addr) 140737488355328))
             (rb nbytes addr r-x x86)
           (mv 'rml-size 0 x86)))))

Theorem: x86p-of-mv-nth-2-of-rml-size

(defthm x86p-of-mv-nth-2-of-rml-size
  (implies (force (x86p x86))
           (x86p (mv-nth 2 (rml-size bytes lin-addr r-x x86)))))