		Search-engine friendly clone of the ACL2 documentation.

Prefix-modrm-sib-decoding

Compute-mandatory-prefix-for-0f-3a-three-byte-opcode

Signature
(compute-mandatory-prefix-for-0f-3a-three-byte-opcode proc-mode opcode prefixes) → mandatory-prefix
Returns: mandatory-prefix — Type (unsigned-byte-p 8 mandatory-prefix).

Definitions and Theorems

Function: compute-mandatory-prefix-for-0f-3a-three-byte-opcode$inline

(defun compute-mandatory-prefix-for-0f-3a-three-byte-opcode$inline
       (proc-mode opcode prefixes)
  (declare (type (integer 0 4) proc-mode)
           (type (unsigned-byte 8) opcode)
           (type (unsigned-byte 52) prefixes))
  (case proc-mode
    (0 (64-bit-compute-mandatory-prefix-for-0f-3a-three-byte-opcode
            opcode prefixes))
    (otherwise (32-bit-compute-mandatory-prefix-for-0f-3a-three-byte-opcode
                    opcode prefixes))))

Theorem: return-type-of-compute-mandatory-prefix-for-0f-3a-three-byte-opcode

(defthm
 return-type-of-compute-mandatory-prefix-for-0f-3a-three-byte-opcode
 (b* ((mandatory-prefix (compute-mandatory-prefix-for-0f-3a-three-byte-opcode$inline
                             proc-mode opcode prefixes)))
   (unsigned-byte-p 8 mandatory-prefix))
 :rule-classes :rewrite)