		Search-engine friendly clone of the ACL2 documentation.

Modr/m-decoding

32-bit-mode-one-byte-opcode-modr/m-p

Returns a boolean saying whether, in 32-bit mode, the given opcode in the one-byte opcode map expects a ModR/M byte.

Signature
(32-bit-mode-one-byte-opcode-modr/m-p opcode) → bool
Returns: bool — Type (booleanp bool), given (n08p opcode).

Definitions and Theorems

Function: 32-bit-mode-one-byte-opcode-modr/m-p$inline

(defun 32-bit-mode-one-byte-opcode-modr/m-p$inline (opcode)
  (declare (type (unsigned-byte 8) opcode))
  (aref1 '32-bit-mode-one-byte-has-modr/m
         *32-bit-mode-one-byte-has-modr/m-ar*
         opcode))

Theorem: booleanp-of-32-bit-mode-one-byte-opcode-modr/m-p

(defthm booleanp-of-32-bit-mode-one-byte-opcode-modr/m-p
 (implies
   (n08p opcode)
   (b* ((bool (32-bit-mode-one-byte-opcode-modr/m-p$inline opcode)))
     (booleanp bool)))
 :rule-classes :rewrite)