(good-lin-addr-p lin-addr x86) → *
Function:
(defun good-lin-addr-p (lin-addr x86) (declare (xargs :stobjs (x86))) (declare (xargs :guard t)) (let ((__function__ 'good-lin-addr-p)) (declare (ignorable __function__)) (b* ((cr0 (the (unsigned-byte 32) (n32 (ctri *cr0* x86)))) (cr4 (the (unsigned-byte 22) (n22 (ctri *cr4* x86)))) (ia32-efer (the (unsigned-byte 12) (n12 (msri *ia32_efer-idx* x86))))) (cond ((equal (cr0bits->pg cr0) 0) (n32p lin-addr)) ((equal (cr4bits->pae cr4) 0) (n32p lin-addr)) ((equal (ia32_eferbits->lme ia32-efer) 0) (n32p lin-addr)) (t (canonical-address-p lin-addr))))))