		Search-engine friendly clone of the ACL2 documentation.

Asm-output

Make-asm-output

Basic constructor macro for asm-output structures.

Syntax

(make-asm-output [:name <name>] 
                 [:constraint <constraint>] 
                 [:lvalue <lvalue>])

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

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

Definition

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

Macro: make-asm-output

(defmacro make-asm-output (&rest args)
  (std::make-aggregate 'asm-output
                       args '((:name) (:constraint) (:lvalue))
                       'make-asm-output
                       nil))

Function: asm-output

(defun asm-output (name constraint lvalue)
  (declare (xargs :guard (and (ident-optionp name)
                              (stringlit-listp constraint)
                              (exprp lvalue))))
  (declare (xargs :guard t))
  (b* ((name (mbe :logic (ident-option-fix name)
                  :exec name))
       (constraint (mbe :logic (stringlit-list-fix constraint)
                        :exec constraint))
       (lvalue (mbe :logic (expr-fix lvalue)
                    :exec lvalue)))
    (cons name (cons constraint lvalue))))