		Search-engine friendly clone of the ACL2 documentation.

Instructions

X86-device-not-available

Semantic function corresponding to a device not available (no math coprocessor) fault

Signature
(x86-device-not-available message start-rip temp-rip x86) → x86
Returns: x86 — Type (x86p x86), given (x86p x86).

Note that the #NM (device not available) exception should be thrown here, which is why the fault field is populated with message.

Definitions and Theorems

Function: x86-device-not-available

(defun x86-device-not-available (message start-rip temp-rip x86)
  (declare (xargs :stobjs (x86)))
  (declare (type (signed-byte 48) start-rip)
           (type (signed-byte 48) temp-rip))
  (let ((__function__ 'x86-device-not-available))
    (declare (ignorable __function__))
    (b* ((ctx 'x86-device-not-available)
         (x86 (!rip temp-rip x86)))
      (!!fault-fresh :nm message
                     :instruction-address start-rip))))

Theorem: x86p-of-x86-device-not-available

(defthm x86p-of-x86-device-not-available
 (implies
  (x86p x86)
  (b*
   ((x86 (x86-device-not-available message start-rip temp-rip x86)))
   (x86p x86)))
 :rule-classes :rewrite)