Wiml-size
- Signature
(wiml-size nbytes addr val x86) → (mv * x86)
Definitions and Theorems
Function: wiml-size$inline
(defun wiml-size$inline (nbytes addr val x86)
(declare (xargs :stobjs (x86)))
(declare (type (member 1 2 4 8) nbytes)
(type (signed-byte 48) addr)
(type integer val))
(declare (xargs :guard
(case nbytes
(1 (i08p val))
(2 (i16p val))
(4 (i32p val))
(8 (i64p val)))))
(case nbytes
(1 (wiml08 addr val x86))
(2 (wiml16 addr val x86))
(4 (wiml32 addr val x86))
(8 (wiml64 addr val x86))
(otherwise (mv 'wiml-size x86))))
