		Search-engine friendly clone of the ACL2 documentation.

Ia32e-paging

Page-fault-err-no

Signature
(page-fault-err-no p-flag r-w-x cpl rsvd smep pae nxe) → errno
Returns: errno — Type (natp errno).

Definitions and Theorems

Function: page-fault-err-no

(defun page-fault-err-no (p-flag r-w-x cpl rsvd smep pae nxe)
  (declare (type (unsigned-byte 1) p-flag)
           (type (member :r :w :x) r-w-x)
           (type (unsigned-byte 2) cpl)
           (type (unsigned-byte 1) rsvd)
           (type (unsigned-byte 1) smep)
           (type (unsigned-byte 1) pae)
           (type (unsigned-byte 1) nxe))
  (let ((__function__ 'page-fault-err-no))
    (declare (ignorable __function__))
    (logior (if (equal p-flag 1) 1 0)
            (if (equal r-w-x :w) 2 0)
            (if (equal cpl 3) 4 0)
            (if (equal rsvd 1) 8 0)
            (if (and (equal r-w-x :x)
                     (or (equal smep 1)
                         (and (equal pae 1) (equal nxe 1))))
                16
              0))))

Theorem: natp-of-page-fault-err-no

(defthm natp-of-page-fault-err-no
  (b*
    ((errno (page-fault-err-no p-flag r-w-x cpl rsvd smep pae nxe)))
    (natp errno))
  :rule-classes :type-prescription)