		Search-engine friendly clone of the ACL2 documentation.

Physical-memory

Create-physical-address-list

Signature
(create-physical-address-list count addr) → *

Given a physical address addr, create-physical-address-list creates a list of physical addresses where the first address is addr and the last address is the last physical address in the range addr to addr + count.

Definitions and Theorems

Function: create-physical-address-list

(defun create-physical-address-list (count addr)
  (declare (xargs :guard (and (natp count)
                              (physical-address-p addr)
                              (physical-address-p (+ addr count)))))
  (let ((__function__ 'create-physical-address-list))
    (declare (ignorable __function__))
    (if (or (zp count)
            (not (physical-address-p addr)))
        nil
      (cons addr
            (create-physical-address-list (1- count)
                                          (1+ addr))))))

Theorem: physical-address-listp-create-physical-address-list

(defthm physical-address-listp-create-physical-address-list
  (physical-address-listp (create-physical-address-list count addr))
  :rule-classes (:rewrite :type-prescription))