		Search-engine friendly clone of the ACL2 documentation.

State-stobj

Read1-memory-unsigned16

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

Definitions and Theorems

Function: read1-memory-unsigned16

(defun read1-memory-unsigned16 (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-unsigned16))
    (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)))
            (cond ((feat-little-endianp feat)
                   (logapp 8 b0 (logapp 8 b1 0)))
                  ((feat-big-endianp feat)
                   (logapp 8 b1 (logapp 8 b0 0)))
                  (t (acl2::impossible-fn)))))
      0)))