		Search-engine friendly clone of the ACL2 documentation.

State-stobj

Read1-memory-unsigned8

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

Definitions and Theorems

Function: read1-memory-unsigned8

(defun read1-memory-unsigned8 (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-unsigned8))
    (declare (ignorable __function__))
    (if (mbt (stat1p stat1))
        (b* ((stat (stat-from-stat1 stat1)))
          (let* ((addr (loghead (feat->xlen feat) addr)))
            (ubyte8-fix (nth addr (stat->memory stat)))))
      0)))