		Search-engine friendly clone of the ACL2 documentation.

Asm-stmt

Make-asm-stmt

Basic constructor macro for asm-stmt structures.

Syntax

(make-asm-stmt [:uscores <uscores>] 
               [:quals <quals>] 
               [:template <template>] 
               [:num-colons <num-colons>] 
               [:outputs <outputs>] 
               [:inputs <inputs>] 
               [:clobbers <clobbers>] 
               [:labels <labels>])

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

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

Definition

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

Macro: make-asm-stmt

(defmacro make-asm-stmt (&rest args)
  (std::make-aggregate 'asm-stmt
                       args
                       '((:uscores)
                         (:quals)
                         (:template)
                         (:num-colons)
                         (:outputs)
                         (:inputs)
                         (:clobbers)
                         (:labels))
                       'make-asm-stmt
                       nil))

Function: asm-stmt

(defun asm-stmt (uscores quals template num-colons
                         outputs inputs clobbers labels)
  (declare (xargs :guard (and (keyword-uscores-p uscores)
                              (asm-qual-listp quals)
                              (stringlit-listp template)
                              (natp num-colons)
                              (asm-output-listp outputs)
                              (asm-input-listp inputs)
                              (asm-clobber-listp clobbers)
                              (ident-listp labels))))
  (declare (xargs :guard t))
  (b* ((uscores (mbe :logic (keyword-uscores-fix uscores)
                     :exec uscores))
       (quals (mbe :logic (asm-qual-list-fix quals)
                   :exec quals))
       (template (mbe :logic (stringlit-list-fix template)
                      :exec template))
       (num-colons (mbe :logic (nfix num-colons)
                        :exec num-colons))
       (outputs (mbe :logic (asm-output-list-fix outputs)
                     :exec outputs))
       (inputs (mbe :logic (asm-input-list-fix inputs)
                    :exec inputs))
       (clobbers (mbe :logic (asm-clobber-list-fix clobbers)
                      :exec clobbers))
       (labels (mbe :logic (ident-list-fix labels)
                    :exec labels)))
    (cons (cons (cons uscores quals)
                (cons template num-colons))
          (cons (cons outputs inputs)
                (cons clobbers labels)))))