		Search-engine friendly clone of the ACL2 documentation.

State32

Make-state32

Basic constructor macro for state32 structures.

Syntax

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

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

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

Definition

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

Macro: make-state32

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

Function: state32

(defun state32 (xregfile pc mem error)
  (declare (xargs :guard (and (xregfile32p xregfile)
                              (ubyte32p pc)
                              (memory32p mem)
                              (booleanp error))))
  (declare (xargs :guard t))
  (let ((__function__ 'state32))
    (declare (ignorable __function__))
    (b* ((xregfile (mbe :logic (xregfile32-fix xregfile)
                        :exec xregfile))
         (pc (mbe :logic (ubyte32-fix pc) :exec pc))
         (mem (mbe :logic (memory32-fix mem)
                   :exec mem))
         (error (mbe :logic (acl2::bool-fix error)
                     :exec error)))
      (cons :state32 (list xregfile pc mem error)))))