		Search-engine friendly clone of the ACL2 documentation.

State-stobj

Write1-xreg

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

Definitions and Theorems

Function: write1-xreg

(defun write1-xreg (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)
                              (stat-validp stat feat)
                              (< (lnfix reg) (feat->xnum feat)))))))
 (prog2$
  (acl2::throw-nonexec-error 'write1-xreg
                             (list reg val stat1 feat))
  (let ((__function__ 'write1-xreg))
   (declare (ignorable __function__))
   (if
    (mbt (stat1p stat1))
    (stat1-from-stat
     (b* ((stat (stat-from-stat1 stat1)))
      (let* ((reg (lnfix reg)))
       (if (= reg 0)
           (stat-fix stat)
         (let
           ((change-stat stat)
            (stat->xregs (update-nth (+ -1 reg)
                                     (loghead (feat->xlen feat) val)
                                     (stat->xregs stat))))
           (stat stat->xregs (stat->pc change-stat)
                 (stat->memory change-stat)
                 (stat->error change-stat)))))))
    stat1))))