		Search-engine friendly clone of the ACL2 documentation.

Gen-addressing-method-code-doc

Signature
(gen-addressing-method-code-doc z-info) → *
Arguments: z-info — Guard (alistp z-info).

Definitions and Theorems

Function: get-addressing-method-doc

(defun get-addressing-method-doc (code)
  (declare (xargs :guard (addressing-method-code-p code)))
  (let ((__function__ 'get-addressing-method-doc))
    (declare (ignorable __function__))
    (b* ((alst (cdr (assoc-equal code *z-addressing-method-info*)))
         (doc (cdr (assoc-equal :doc alst)))
         ((unless doc) ""))
      doc)))

Theorem: stringp-of-get-addressing-method-doc

(defthm stringp-of-get-addressing-method-doc
  (b* ((str (get-addressing-method-doc code)))
    (stringp str))
  :rule-classes :rewrite)

Function: gen-addressing-method-code-doc

(defun gen-addressing-method-code-doc (z-info)
 (declare (xargs :guard (alistp z-info)))
 (let ((__function__ 'gen-addressing-method-code-doc))
  (declare (ignorable __function__))
  (if (endp z-info)
      nil
    (b*
     ((code (caar z-info))
      ((unless (addressing-method-code-p code))
       (er hard? __function__
           "~% Bad code ~x0 encountered! ~%" code))
      (codestr (str::pretty code
                            :config *x86isa-printconfig-base-10*))
      (docstr (str::cat "@(' " codestr "'): "
                        (get-addressing-method-doc code)))
      (topic-name (intern$ (str::cat codestr "-Z-ADDRESSING-METHOD")
                           "X86ISA"))
      (form (cons (cons 'defxdoc
                        (cons topic-name
                              (cons ':long (cons docstr 'nil))))
                  'nil))
      (rest (gen-addressing-method-code-doc (cdr z-info))))
     (append form rest)))))