		Search-engine friendly clone of the ACL2 documentation.

State-stobj

Read1-memory-unsigned32

Signature
(read1-memory-unsigned32 addr stat1 feat) → *

Definitions and Theorems

Function: read1-memory-unsigned32

(defun read1-memory-unsigned32 (addr stat1 feat)
 (declare (xargs :stobjs (stat1)))
 (declare (xargs :guard (and (stat1p stat1)
                             (b* ((stat (stat-from-stat1 stat1)))
                               (and (integerp addr)
                                    (statp stat)
                                    (featp feat)
                                    (stat-validp stat feat))))))
 (let ((__function__ 'read1-memory-unsigned32))
   (declare (ignorable __function__))
   (if
    (mbt (stat1p stat1))
    (b* ((stat (stat-from-stat1 stat1)))
      (let* ((b0 (read-memory-unsigned8 addr stat feat))
             (b1 (read-memory-unsigned8 (+ (lifix addr) 1)
                                        stat feat))
             (b2 (read-memory-unsigned8 (+ (lifix addr) 2)
                                        stat feat))
             (b3 (read-memory-unsigned8 (+ (lifix addr) 3)
                                        stat feat)))
        (cond ((feat-little-endianp feat)
               (logapp 8 b0
                       (logapp 8 b1 (logapp 8 b2 (logapp 8 b3 0)))))
              ((feat-big-endianp feat)
               (logapp 8 b3
                       (logapp 8 b2 (logapp 8 b1 (logapp 8 b0 0)))))
              (t (acl2::impossible-fn)))))
    0)))