(page-fault-err-no p-flag r-w-x cpl rsvd smep pae nxe) → errno
Function:
(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:
(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)