|
|
|---|
|
|
|
|---|
Raw constructor for honsed cpuid-info-p structures.
Syntax:
(honsed-cpuid-info eax ebx ecx edx)
This is identical to cpuid-info, except that we hons the structure we are creating.
This is an ordinary honsing constructor introduced by defaggregate.
Function:
(defun honsed-cpuid-info (eax ebx ecx edx) (declare (xargs :guard (and (unsigned-byte-p 32 eax) (unsigned-byte-p 32 ebx) (unsigned-byte-p 32 ecx) (unsigned-byte-p 32 edx)))) (mbe :logic (cpuid-info eax ebx ecx edx) :exec (hons (hons 'eax eax) (hons (hons 'ebx ebx) (hons (hons 'ecx ecx) (hons (hons 'edx edx) nil))))))