		Search-engine friendly clone of the ACL2 documentation.

State-stobj

Read1-pc

Signature
(read1-pc stat1 feat) → *

Definitions and Theorems

Function: read1-pc

(defun read1-pc (stat1 feat)
  (declare (xargs :stobjs (stat1)))
  (declare (xargs :guard (and (stat1p stat1)
                              (b* ((stat (stat-from-stat1 stat1)))
                                (and (statp stat)
                                     (featp feat)
                                     (stat-validp stat feat))))))
  (let ((__function__ 'read1-pc))
    (declare (ignorable __function__))
    (if (mbt (stat1p stat1))
        (b* ((stat (stat-from-stat1 stat1)))
          (unsigned-byte-fix (feat->xlen feat)
                             (stat->pc stat)))
      0)))