		Search-engine friendly clone of the ACL2 documentation.

Modr/m-decoding

One-byte-opcode-modr/m-p

Returns t if a one-byte opcode requires a ModR/M byte; nil otherwise

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

Definitions and Theorems

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

(defun one-byte-opcode-modr/m-p$inline (proc-mode opcode)
  (declare (type (integer 0 4) proc-mode)
           (type (unsigned-byte 8) opcode))
  (if (equal proc-mode 0)
      (64-bit-mode-one-byte-opcode-modr/m-p opcode)
    (32-bit-mode-one-byte-opcode-modr/m-p opcode)))

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

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