		Search-engine friendly clone of the ACL2 documentation.

Backtrace-frame

Make-backtrace-frame

Basic constructor macro for backtrace-frame structures.

Syntax

(make-backtrace-frame [:index <index>] 
                      [:rune <rune>] 
                      [:objs <objs>])

This is the usual way to construct backtrace-frame structures. It simply conses together a structure with the specified fields.

This macro generates a new backtrace-frame structure from scratch. See also change-backtrace-frame, which can "change" an existing structure, instead.

Definition

This is an ordinary make- macro introduced by defprod.

Macro: make-backtrace-frame

(defmacro make-backtrace-frame (&rest args)
  (std::make-aggregate 'backtrace-frame
                       args '((:index) (:rune) (:objs))
                       'make-backtrace-frame
                       nil))

Function: backtrace-frame

(defun backtrace-frame (index rune objs)
  (declare (xargs :guard (and (natp index)
                              (maybe-fgl-generic-rune-p rune)
                              (fgl-object-bindings-p objs))))
  (declare (xargs :guard t))
  (let ((__function__ 'backtrace-frame))
    (declare (ignorable __function__))
    (b* ((index (mbe :logic (nfix index) :exec index))
         (rune (mbe :logic (maybe-fgl-generic-rune-fix rune)
                    :exec rune))
         (objs (mbe :logic (fgl-object-bindings-fix objs)
                    :exec objs)))
      (list index rune objs))))