		Search-engine friendly clone of the ACL2 documentation.

Instructions

X86-step-unimplemented

Semantic function corresponding to Intel's instructions unsupported in the x86isa books

Signature
(x86-step-unimplemented message x86) → x86
Returns: x86 — Type (x86p x86), given (x86p x86).

Note that the ms field is populated with message here because this function is called when a model-related error occurs.

Definitions and Theorems

Function: x86-step-unimplemented

(defun x86-step-unimplemented (message x86)
  (declare (xargs :stobjs (x86)))
  (declare (xargs :guard t))
  (let ((__function__ 'x86-step-unimplemented))
    (declare (ignorable __function__))
    (b* ((ctx 'x86-step-unimplemented))
      (!!ms-fresh :message message))))

Theorem: x86p-of-x86-step-unimplemented

(defthm x86p-of-x86-step-unimplemented
  (implies (x86p x86)
           (b* ((x86 (x86-step-unimplemented message x86)))
             (x86p x86)))
  :rule-classes :rewrite)