Xcr0bits-debug
- Signature
(xcr0bits-debug x) → *
- Arguments
- x — Guard (xcr0bits-p x).
Definitions and Theorems
Function: xcr0bits-debug$inline
(defun xcr0bits-debug$inline (x)
(declare (xargs :guard (xcr0bits-p x)))
(b* (((xcr0bits x)))
(cons
(cons 'fpu/mmx-state x.fpu/mmx-state)
(cons
(cons 'sse-state x.sse-state)
(cons
(cons 'avx-state x.avx-state)
(cons
(cons 'bndreg-state x.bndreg-state)
(cons
(cons 'bndcsr-state x.bndcsr-state)
(cons
(cons 'opmask-state x.opmask-state)
(cons
(cons 'zmm_hi256-state
x.zmm_hi256-state)
(cons
(cons 'hi16_zmm-state x.hi16_zmm-state)
(cons
(cons 'res1 x.res1)
(cons
(cons 'pkru-state x.pkru-state)
(cons
(cons 'res2 x.res2)
(cons (cons 'tileconfig-state
x.tileconfig-state)
(cons (cons 'tiledata-state x.tiledata-state)
(cons (cons 'res4 x.res4)
nil))))))))))))))))
