		Search-engine friendly clone of the ACL2 documentation.

State-stobj

Write1-memory-unsigned8

Signature
(write1-memory-unsigned8 addr val stat1 feat) → *

Definitions and Theorems

Function: write1-memory-unsigned8

(defun write1-memory-unsigned8 (addr val stat1 feat)
 (declare (xargs :stobjs (stat1)))
 (declare (xargs :non-executable t
                 :guard (and (stat1p stat1)
                             (b* ((stat (stat-from-stat1 stat1)))
                               (and (integerp addr)
                                    (ubyte8p val)
                                    (statp stat)
                                    (featp feat)
                                    (stat-validp stat feat))))))
 (prog2$
  (acl2::throw-nonexec-error 'write1-memory-unsigned8
                             (list addr val stat1 feat))
  (let ((__function__ 'write1-memory-unsigned8))
    (declare (ignorable __function__))
    (if
     (mbt (stat1p stat1))
     (stat1-from-stat
          (b* ((stat (stat-from-stat1 stat1)))
            (let* ((addr (loghead (feat->xlen feat) addr)))
              (let ((change-stat stat)
                    (stat->memory (update-nth addr (ubyte8-fix val)
                                              (stat->memory stat))))
                (stat (stat->xregs change-stat)
                      (stat->pc change-stat)
                      stat->memory
                      (stat->error change-stat))))))
     stat1))))