(ia32e-pde-2mb-pagebits-debug x) → *
Function:
(defun ia32e-pde-2mb-pagebits-debug (x) (declare (xargs :guard (ia32e-pde-2mb-pagebits-p x))) (let ((__function__ 'ia32e-pde-2mb-pagebits-debug)) (declare (ignorable __function__)) (b* (((ia32e-pde-2mb-pagebits x))) (cons (cons 'p x.p) (cons (cons 'r/w x.r/w) (cons (cons 'u/s x.u/s) (cons (cons 'pwt x.pwt) (cons (cons 'pcd x.pcd) (cons (cons 'a x.a) (cons (cons 'd x.d) (cons (cons 'ps x.ps) (cons (cons 'g x.g) (cons (cons 'res1 x.res1) (cons (cons 'pat x.pat) (cons (cons 'res2 x.res2) (cons (cons 'page x.page) (cons (cons 'res3 x.res3) (cons (cons 'xd x.xd) nil))))))))))))))))))