		Search-engine friendly clone of the ACL2 documentation.

Program-execution

Gdt-entry

Signature
(gdt-entry flags base limit) → entry
Returns: entry — Type (n64p entry).

Definitions and Theorems

Function: gdt-entry

(defun gdt-entry (flags base limit)
  (declare (type (unsigned-byte 16) flags)
           (type (unsigned-byte 32) base)
           (type (unsigned-byte 20) limit))
  (let ((__function__ 'gdt-entry))
    (declare (ignorable __function__))
    (logior (ash (logand base 4278190080) (- 56 24))
            (ash (logand flags 61695) 40)
            (ash (logand limit 983040) (- 48 16))
            (ash (logand base 16777215) 16)
            (logand limit 65535))))

Theorem: n64p-of-gdt-entry

(defthm n64p-of-gdt-entry
  (b* ((entry (gdt-entry flags base limit)))
    (n64p entry))
  :rule-classes :rewrite)