		Search-engine friendly clone of the ACL2 documentation.

State64

Make-state64

Basic constructor macro for state64 structures.

Syntax

(make-state64 [:xregfile <xregfile>] 
              [:pc <pc>] 
              [:mem <mem>] 
              [:error <error>])

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

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

Definition

This is an ordinary make- macro introduced by fty::defprod.

Macro: make-state64

(defmacro make-state64 (&rest args)
  (std::make-aggregate 'state64
                       args
                       '((:xregfile) (:pc) (:mem) (:error))
                       'make-state64
                       nil))

Function: state64

(defun state64 (xregfile pc mem error)
  (declare (xargs :guard (and (xregfile64p xregfile)
                              (ubyte64p pc)
                              (memory64p mem)
                              (booleanp error))))
  (declare (xargs :guard t))
  (let ((__function__ 'state64))
    (declare (ignorable __function__))
    (b* ((xregfile (mbe :logic (xregfile64-fix xregfile)
                        :exec xregfile))
         (pc (mbe :logic (ubyte64-fix pc) :exec pc))
         (mem (mbe :logic (memory64-fix mem)
                   :exec mem))
         (error (mbe :logic (acl2::bool-fix error)
                     :exec error)))
      (cons :state64 (list xregfile pc mem error)))))