Basic constructor macro for stat32i structures.
(make-stat32i [:xregs <xregs>] [:pc <pc>] [:memory <memory>] [:error <error>])
This is the usual way to construct stat32i structures. It simply conses together a structure with the specified fields.
This macro generates a new stat32i structure from scratch. See also change-stat32i, which can "change" an existing structure, instead.
This is an ordinary
Macro:
(defmacro make-stat32i (&rest args) (std::make-aggregate 'stat32i args '((:xregs) (:pc) (:memory) (:error)) 'make-stat32i nil))
Function:
(defun stat32i (xregs pc memory error) (declare (xargs :guard (and (xregs32ip xregs) (ubyte32p pc) (memory32ip memory) (booleanp error)))) (declare (xargs :guard t)) (let ((__function__ 'stat32i)) (declare (ignorable __function__)) (b* ((xregs (mbe :logic (xregs32i-fix xregs) :exec xregs)) (pc (mbe :logic (ubyte32-fix pc) :exec pc)) (memory (mbe :logic (memory32i-fix memory) :exec memory)) (error (mbe :logic (acl2::bool-fix error) :exec error))) (list (cons 'xregs xregs) (cons 'pc pc) (cons 'memory memory) (cons 'error error)))))