		Search-engine friendly clone of the ACL2 documentation.

Linear-memory

Riml-size

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

Definitions and Theorems

Function: riml-size$inline

(defun riml-size$inline (nbytes addr r-x x86)
  (declare (xargs :stobjs (x86)))
  (declare (type (member 1 2 4 8) nbytes)
           (type (signed-byte 48) addr)
           (type (member :r :x) r-x))
  (case nbytes
    (1 (riml08 addr r-x x86))
    (2 (riml16 addr r-x x86))
    (4 (riml32 addr r-x x86))
    (8 (riml64 addr r-x x86))
    (otherwise (mv 'riml-size nbytes x86))))