		Search-engine friendly clone of the ACL2 documentation.

Vl-server

Vls-data-from-zip

Signature
(vls-data-from-zip zip) → data
Arguments: zip — Guard (vl-zipfile-p zip).
Returns: data — Type (vls-data-p data).

Definitions and Theorems

Function: vls-data-from-zip

(defun vls-data-from-zip (zip)
 (declare (xargs :guard (vl-zipfile-p zip)))
 (let ((__function__ 'vls-data-from-zip))
  (declare (ignorable __function__))
  (b*
   (((vl-zipfile zip))
    (orig
     (cwtime
      (hons-copy
       (cwtime
         (vl-annotate-design zip.design *vl-default-simpconfig*)))))
    (orig-descalist
         (fast-alist-free
              (vl-make-descalist (vl-design-descriptions orig)))))
   (make-vls-data :name zip.name
                  :date zip.date
                  :ltime zip.ltime
                  :orig orig
                  :orig-descalist orig-descalist
                  :filemap zip.filemap
                  :defs zip.defines))))

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

(defthm vls-data-p-of-vls-data-from-zip
  (b* ((data (vls-data-from-zip zip)))
    (vls-data-p data))
  :rule-classes :rewrite)