		Search-engine friendly clone of the ACL2 documentation.

Server

Vls-data-from-translation

Signature
(vls-data-from-translation trans) → data
Arguments: trans — Guard (vl-translation-p trans).
Returns: data — Type (vls-data-p data), given the guard.

Definitions and Theorems

Function: vls-data-from-translation

(defun vls-data-from-translation (trans)
 (declare (xargs :guard (vl-translation-p trans)))
 (let ((__function__ 'vls-data-from-translation))
  (declare (ignorable __function__))
  (b*
   (((vl-translation trans) trans)
    (orig
      (cwtime (hons-copy (cwtime (vl-annotate-design trans.orig)))))
    (orig-descalist
         (fast-alist-free
              (vl-make-descalist (vl-design-descriptions orig)))))
   (make-vls-data :good trans.good
                  :bad trans.bad
                  :orig orig
                  :orig-descalist orig-descalist
                  :filemap trans.filemap
                  :defs trans.defines))))

Theorem: vls-data-p-of-vls-data-from-translation

(defthm vls-data-p-of-vls-data-from-translation
  (implies (and (vl-translation-p trans))
           (b* ((data (vls-data-from-translation trans)))
             (vls-data-p data)))
  :rule-classes :rewrite)