		Search-engine friendly clone of the ACL2 documentation.

Instructions

X86-general-protection

Semantic function corresponding to a general protection fault

Signature
(x86-general-protection message start-rip temp-rip x86) → x86
Returns: x86 — Type (x86p x86), given (x86p x86).

Note that the #GP (general protection) exception should be thrown here, which is why the fault field is populated with message.

Definitions and Theorems

Function: x86-general-protection

(defun x86-general-protection (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-general-protection))
    (declare (ignorable __function__))
    (b* ((ctx 'x86-general-protection)
         (x86 (!rip temp-rip x86)))
      (!!fault-fresh :gp message
                     :instruction-address start-rip))))

Theorem: x86p-of-x86-general-protection

(defthm x86p-of-x86-general-protection
 (implies
   (x86p x86)
   (b*
     ((x86 (x86-general-protection message start-rip temp-rip x86)))
     (x86p x86)))
 :rule-classes :rewrite)