		Search-engine friendly clone of the ACL2 documentation.

State-stobj

Error1

Signature
(error1 stat1 feat) → *

Definitions and Theorems

Function: error1

(defun error1 (stat1 feat)
 (declare (xargs :stobjs (stat1)))
 (declare (xargs :non-executable t
                 :guard (and (stat1p stat1)
                             (b* ((stat (stat-from-stat1 stat1)))
                               (and (statp stat)
                                    (featp feat)
                                    (stat-validp stat feat))))))
 (prog2$
  (acl2::throw-nonexec-error 'error1
                             (list stat1 feat))
  (let ((__function__ 'error1))
    (declare (ignorable __function__))
    (if (mbt (stat1p stat1))
        (stat1-from-stat (b* ((stat (stat-from-stat1 stat1)))
                           (let ((change-stat stat) (stat->error t))
                             (stat (stat->xregs change-stat)
                                   (stat->pc change-stat)
                                   (stat->memory change-stat)
                                   stat->error))))
      stat1))))