		Search-engine friendly clone of the ACL2 documentation.

Ia32-segmentation

Ia32-valid-code-segment-descriptor-p

Recognizer for a valid code segment descriptor in 32-bit mode

Signature
(ia32-valid-code-segment-descriptor-p descriptor) → (mv * *)

Definitions and Theorems

Function: ia32-valid-code-segment-descriptor-p

(defun ia32-valid-code-segment-descriptor-p (descriptor)
 (declare (type (unsigned-byte 64) descriptor))
 (let ((__function__ 'ia32-valid-code-segment-descriptor-p))
  (declare (ignorable __function__))
  (b*
   (((when
      (not
        (equal (code-segment-descriptorbits->msb-of-type descriptor)
               1)))
     (mv nil
         (cons :invalid-segment-type descriptor)))
    ((when (not (equal (code-segment-descriptorbits->s descriptor)
                       1)))
     (mv nil
         (cons :invalid-segment-type descriptor)))
    ((when (not (equal (code-segment-descriptorbits->p descriptor)
                       1)))
     (mv nil
         (cons :segment-not-present descriptor)))
    ((when (not (equal (code-segment-descriptorbits->l descriptor)
                       0)))
     (mv nil (cons :ia32e-mode-off descriptor))))
   (mv t 0))))