		Search-engine friendly clone of the ACL2 documentation.

Ia32e-paging

Good-lin-addr-p

Signature
(good-lin-addr-p lin-addr x86) → *

Definitions and Theorems

Function: good-lin-addr-p

(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))))))