• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Community
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
    • Sv
    • Fgl
    • Vwsim
    • Vl
      • Syntax
      • Loader
      • Warnings
      • Getting-started
      • Utilities
      • Printer
      • Kit
        • Vl-lint
        • Vl-server
        • Vl-gather
        • Vl-zip
          • Vl-zip-opts-p
          • Vl-zipfile
            • Vl-zipfile-fix
            • Vl-read-zip-header
              • Vl-read-zip-header-aux
              • Vl-read-zip-aux
            • Vl-maybe-zipfile
            • Vl-read-zip
            • Make-vl-zipfile
            • Vl-zipfile-equiv
            • Vl-zipfile-p
            • Change-vl-zipfile
            • Vl-zipfile->syntax
            • Vl-zipfile->filemap
            • Vl-zipfile->design
            • Vl-zipfile->defines
            • Vl-zipfile->name
            • Vl-zipfile->ltime
            • Vl-zipfile->date
            • Vl-write-zip
          • *vl-zip-help*
          • Vl-zip-top
          • Vl-zip-main
        • Vl-main
        • Split-plusargs
        • Vl-shell
        • Vl-json
      • Mlib
      • Transforms
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Vl-zipfile

Vl-read-zip-header

Read only the header information out of a vlzip file.

Signature

(vl-read-zip-header filename &key (state 'state)) 
  → 
(mv name syntax date ltime state)

Arguments

filename — Guard (stringp filename).

Returns

name — Type (maybe-stringp name).

syntax — Type (maybe-stringp syntax).

date — Type (maybe-stringp date).

ltime — Type (maybe-natp ltime).

state — Type (state-p1 state), given (state-p1 state).

This should be relatively fast; it doesn't have to read the whole file.

Definitions and Theorems

Function: vl-read-zip-header-fn

(defun vl-read-zip-header-fn (filename state)
  (declare (xargs :stobjs (state)))
  (declare (xargs :guard (stringp filename)))
  (let ((__function__ 'vl-read-zip-header))
    (declare (ignorable __function__))
    (b* ((filename (string-fix filename))
         ((mv channel state)
          (open-input-channel filename
                              :object state))
         ((unless channel)
          (mv nil nil nil nil state))
         ((mv name syntax date ltime state)
          (vl-read-zip-header-aux channel
                                  :name nil
                                  :syntax nil
                                  :date nil
                                  :ltime nil))
         (state (close-input-channel channel state)))
      (mv name syntax date ltime state))))

Theorem: maybe-stringp-of-vl-read-zip-header.name

(defthm maybe-stringp-of-vl-read-zip-header.name
  (b* (((mv ?name ?syntax ?date ?ltime acl2::?state)
        (vl-read-zip-header-fn filename state)))
    (maybe-stringp name))
  :rule-classes :type-prescription)

Theorem: maybe-stringp-of-vl-read-zip-header.syntax

(defthm maybe-stringp-of-vl-read-zip-header.syntax
  (b* (((mv ?name ?syntax ?date ?ltime acl2::?state)
        (vl-read-zip-header-fn filename state)))
    (maybe-stringp syntax))
  :rule-classes :type-prescription)

Theorem: maybe-stringp-of-vl-read-zip-header.date

(defthm maybe-stringp-of-vl-read-zip-header.date
  (b* (((mv ?name ?syntax ?date ?ltime acl2::?state)
        (vl-read-zip-header-fn filename state)))
    (maybe-stringp date))
  :rule-classes :type-prescription)

Theorem: maybe-natp-of-vl-read-zip-header.ltime

(defthm maybe-natp-of-vl-read-zip-header.ltime
  (b* (((mv ?name ?syntax ?date ?ltime acl2::?state)
        (vl-read-zip-header-fn filename state)))
    (maybe-natp ltime))
  :rule-classes :type-prescription)

Theorem: state-p1-of-vl-read-zip-header.state

(defthm state-p1-of-vl-read-zip-header.state
  (implies (state-p1 state)
           (b* (((mv ?name ?syntax ?date ?ltime acl2::?state)
                 (vl-read-zip-header-fn filename state)))
             (state-p1 state)))
  :rule-classes :rewrite)

Subtopics

Vl-read-zip-header-aux

Vl-read-zip-aux