		Search-engine friendly clone of the ACL2 documentation.
State-stobj
Write1-memory-unsigned64

Signature
(write1-memory-unsigned64 addr val stat1 feat) → *
Definitions and Theorems

Function: write1-memory-unsigned64
(defun write1-memory-unsigned64 (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)
                                    (ubyte64p val)
                                    (statp stat)
                                    (featp feat)
                                    (stat-validp stat feat))))))
 (prog2$
  (acl2::throw-nonexec-error 'write1-memory-unsigned64
                             (list addr val stat1 feat))
  (let ((__function__ 'write1-memory-unsigned64))
   (declare (ignorable __function__))
   (if
    (mbt (stat1p stat1))
    (stat1-from-stat
     (b* ((stat (stat-from-stat1 stat1)))
      (let* ((val (ubyte64-fix val))
             (b0 (bitops::part-select-width-low val 8 0))
             (b1 (bitops::part-select-width-low val 8 8))
             (b2 (bitops::part-select-width-low val 8 16))
             (b3 (bitops::part-select-width-low val 8 24))
             (b4 (bitops::part-select-width-low val 8 32))
             (b5 (bitops::part-select-width-low val 8 40))
             (b6 (bitops::part-select-width-low val 8 48))
             (b7 (bitops::part-select-width-low val 8 56)))
       (mv-let (1st-byte 2nd-byte 3rd-byte 4th-byte
                         5th-byte 6th-byte 7th-byte 8th-byte)
               (if (feat-little-endianp feat)
                   (mv b0 b1 b2 b3 b4 b5 b6 b7)
                 (mv b7 b6 b5 b4 b3 b2 b1 b0))
         (let*
            ((stat (write-memory-unsigned8 addr 1st-byte stat feat))
             (stat (write-memory-unsigned8 (+ (lifix addr) 1)
                                           2nd-byte stat feat))
             (stat (write-memory-unsigned8 (+ (lifix addr) 2)
                                           3rd-byte stat feat))
             (stat (write-memory-unsigned8 (+ (lifix addr) 3)
                                           4th-byte stat feat))
             (stat (write-memory-unsigned8 (+ (lifix addr) 4)
                                           5th-byte stat feat))
             (stat (write-memory-unsigned8 (+ (lifix addr) 5)
                                           6th-byte stat feat))
             (stat (write-memory-unsigned8 (+ (lifix addr) 6)
                                           7th-byte stat feat))
             (stat (write-memory-unsigned8 (+ (lifix addr) 7)
                                           8th-byte stat feat)))
           stat)))))
    stat1))))