		Search-engine friendly clone of the ACL2 documentation.

State-stobj

Read1-xreg-unsigned

Signature
(read1-xreg-unsigned reg stat1 feat) → *

Definitions and Theorems

Function: read1-xreg-unsigned

(defun read1-xreg-unsigned (reg stat1 feat)
 (declare (xargs :stobjs (stat1)))
 (declare
    (xargs :guard (and (stat1p stat1)
                       (b* ((stat (stat-from-stat1 stat1)))
                         (and (natp reg)
                              (statp stat)
                              (featp feat)
                              (stat-validp stat feat)
                              (< (lnfix reg) (feat->xnum feat)))))))
 (let ((__function__ 'read1-xreg-unsigned))
   (declare (ignorable __function__))
   (if
    (mbt (stat1p stat1))
    (b* ((stat (stat-from-stat1 stat1)))
      (let* ((reg (lnfix reg)))
        (if (= reg 0)
            0
          (unsigned-byte-fix (feat->xlen feat)
                             (nth (+ -1 reg) (stat->xregs stat))))))
    0)))