		Search-engine friendly clone of the ACL2 documentation.

Backtraces

Interp-st-stack-backtrace

Collect a backtrace object from the FGL rewriter stack, given a list of rule specifications

Signature
(interp-st-stack-backtrace specs interp-st) → backtrace
Arguments: specs — Guard (backtrace-speclist-p specs).
Returns: backtrace — Type (backtrace-p backtrace).

Definitions and Theorems

Function: interp-st-stack-backtrace

(defun interp-st-stack-backtrace (specs interp-st)
  (declare (xargs :stobjs (interp-st)))
  (declare (xargs :guard (backtrace-speclist-p specs)))
  (let ((__function__ 'interp-st-stack-backtrace))
    (declare (ignorable __function__))
    (stobj-let ((stack (interp-st->stack interp-st)))
               (bt)
               (stack-backtrace specs stack)
               bt)))

Theorem: backtrace-p-of-interp-st-stack-backtrace

(defthm backtrace-p-of-interp-st-stack-backtrace
  (b* ((backtrace (interp-st-stack-backtrace specs interp-st)))
    (backtrace-p backtrace))
  :rule-classes :rewrite)