(vl-scan-for-zipinfos-aux dir files &key (state 'state)) → (mv infos state)
Function:
(defun vl-scan-for-zipinfos-aux-fn (dir files state) (declare (xargs :stobjs (state))) (declare (xargs :guard (and (stringp dir) (string-listp files)))) (let ((__function__ 'vl-scan-for-zipinfos-aux)) (declare (ignorable __function__)) (b* (((when (atom files)) (mv nil state)) ((mv rest state) (vl-scan-for-zipinfos-aux dir (cdr files))) ((unless (str::strsuffixp ".vlzip" (car files))) (mv rest state)) (shortname (car files)) (fullpath (oslib::catpath dir shortname)) ((ret head) (vl-read-zip-header fullpath)) ((unless (and head.name head.syntax head.date head.ltime)) (cw "; Note: vlzip header problem in ~s0.~%" fullpath) (mv rest state)) (info (make-vl-zipinfo :filename shortname :name head.name :syntax head.syntax :date head.date :ltime head.ltime))) (mv (cons info rest) state))))
Theorem:
(defthm vl-zipinfolist-p-of-vl-scan-for-zipinfos-aux.infos (b* (((mv ?infos acl2::?state) (vl-scan-for-zipinfos-aux-fn dir files state))) (vl-zipinfolist-p infos)) :rule-classes :rewrite)
Theorem:
(defthm state-p1-of-vl-scan-for-zipinfos-aux.state (implies (state-p1 state) (b* (((mv ?infos acl2::?state) (vl-scan-for-zipinfos-aux-fn dir files state))) (state-p1 state))) :rule-classes :rewrite)