		Search-engine friendly clone of the ACL2 documentation.

Tlb-entryp

Recognizer for TLB entries.

Signature
(tlb-entryp x) → *

tlb-entryp recognizes TLB entries, i.e. elements of the the tlb field on the x86 stobj. Each entry is a cons, where the car is a good-tlb-key-p and the cdr is a physical page number.

Definitions and Theorems

Function: tlb-entryp

(defun tlb-entryp (x)
  (declare (xargs :guard t))
  (let ((__function__ 'tlb-entryp))
    (declare (ignorable __function__))
    (b* (((unless (consp x)) nil)
         ((cons key val) x))
      (and (good-tlb-key-p key)
           (unsigned-byte-p (- 52 12) val)))))