		Search-engine friendly clone of the ACL2 documentation.

Physical-memory

Physical-address-p

Signature
(physical-address-p phy-addr) → *

Definitions and Theorems

Function: physical-address-p$inline

(defun physical-address-p$inline (phy-addr)
  (declare (xargs :guard t))
  (mbe :logic (unsigned-byte-p 52 phy-addr)
       :exec (and (integerp phy-addr)
                  (<= 0 phy-addr)
                  (< phy-addr 4503599627370496))))