• Top
  • Documentation
    • Xdoc
      • Undocumented
      • Save
      • Defsection
      • Markup
      • Preprocessor
      • Terminal
      • Emacs-links
      • Defxdoc
      • Katex-integration
      • Constructors
      • Entities
      • Defxdoc+
      • Save-rendered
      • Add-resource-directory
      • Testing
      • Order-subtopics
      • Save-rendered-event
      • Archive-matching-topics
      • Archive-xdoc
      • Xdoc-extend
      • Set-default-parents
      • Missing-parents
        • Interp-st-stack-backtrace-top
        • Interp-st-fn-annotation
        • Interp-st-stack-full-backtrace
        • Missing-parents-test
      • Defpointer
      • Defxdoc-raw
      • Xdoc-tests
      • Xdoc-prepend
      • Defsection-progn
      • Gen-xdoc-for-file
    • ACL2-doc
    • Recursion-and-induction
    • Loop$-primer
    • Operational-semantics
    • Pointers
    • Doc
    • Documentation-copyright
    • Course-materials
    • Publications
    • Args
    • ACL2-doc-summary
    • Finding-documentation
    • Broken-link
    • Doc-terminal-test-2
    • Doc-terminal-test-1
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Community
  • Proof-automation
  • ACL2
  • Macro-libraries
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Missing-parents

Interp-st-stack-backtrace-top

Produce a backtrace frame for the top FGL rewriter stack frame that matches any of a list of rule specifications

Signature

(interp-st-stack-backtrace-top specs interp-st) → frame

Arguments

specs — Guard (backtrace-speclist-p specs).

Returns

frame — Type (iff (backtrace-frame-p frame) frame).

Definitions and Theorems

Function: interp-st-stack-backtrace-top

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

Theorem: return-type-of-interp-st-stack-backtrace-top

(defthm return-type-of-interp-st-stack-backtrace-top
  (b* ((frame (interp-st-stack-backtrace-top specs interp-st)))
    (iff (backtrace-frame-p frame) frame))
  :rule-classes :rewrite)