		Search-engine friendly clone of the ACL2 documentation.

State-stobj

Read1-xreg-signed

Signature
(read1-xreg-signed reg stat1 feat) → *

Definitions and Theorems

Function: read1-xreg-signed

(defun read1-xreg-signed (reg stat1 feat)
 (declare (xargs :stobjs (stat1)))
 (declare
    (xargs :guard (and (stat1p stat1)
                       (b* ((stat (stat-from-stat1 stat1)))
                         (and (natp reg)
                              (statp stat)
                              (featp feat)
                              (stat-validp stat feat)
                              (< (lnfix reg) (feat->xnum feat)))))))
 (let ((__function__ 'read1-xreg-signed))
   (declare (ignorable __function__))
   (if (mbt (stat1p stat1))
       (b* ((stat (stat-from-stat1 stat1)))
         (logext (feat->xlen feat)
                 (read-xreg-unsigned reg stat feat)))
     0)))