		Search-engine friendly clone of the ACL2 documentation.

State-stobj

Write1-xreg-32

Signature
(write1-xreg-32 reg val stat1 feat) → *

Definitions and Theorems

Function: write1-xreg-32

(defun write1-xreg-32 (reg val stat1 feat)
 (declare (xargs :stobjs (stat1)))
 (declare
    (xargs :non-executable t
           :guard (and (stat1p stat1)
                       (b* ((stat (stat-from-stat1 stat1)))
                         (and (natp reg)
                              (integerp val)
                              (statp stat)
                              (featp feat)
                              (feat-64p feat)
                              (stat-validp stat feat)
                              (< (lnfix reg) (feat->xnum feat)))))))
 (prog2$ (acl2::throw-nonexec-error 'write1-xreg-32
                                    (list reg val stat1 feat))
         (let ((__function__ 'write1-xreg-32))
           (declare (ignorable __function__))
           (if (mbt (stat1p stat1))
               (stat1-from-stat (b* ((stat (stat-from-stat1 stat1)))
                                  (write-xreg reg (logext 32 val)
                                              stat feat)))
             stat1))))