• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • 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-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

Make-vl-zipfile

Basic constructor macro for vl-zipfile structures.

Syntax

(make-vl-zipfile [:name <name>] 
                 [:syntax <syntax>] 
                 [:date <date>] 
                 [:ltime <ltime>] 
                 [:design <design>] 
                 [:filemap <filemap>] 
                 [:defines <defines>]) 

This is the usual way to construct vl-zipfile structures. It simply conses together a structure with the specified fields.

This macro generates a new vl-zipfile structure from scratch. See also change-vl-zipfile, which can "change" an existing structure, instead.

Definition

This is an ordinary make- macro introduced by defprod.

Macro: make-vl-zipfile

(defmacro make-vl-zipfile (&rest args)
  (std::make-aggregate 'vl-zipfile
                       args
                       '((:name)
                         (:syntax)
                         (:date)
                         (:ltime)
                         (:design)
                         (:filemap)
                         (:defines))
                       'make-vl-zipfile
                       nil))

Function: vl-zipfile

(defun vl-zipfile (name syntax
                        date ltime design filemap defines)
  (declare (xargs :guard (and (stringp name)
                              (stringp syntax)
                              (stringp date)
                              (natp ltime)
                              (vl-design-p design)
                              (vl-filemap-p filemap)
                              (vl-defines-p defines))))
  (declare (xargs :guard t))
  (let ((__function__ 'vl-zipfile))
    (declare (ignorable __function__))
    (b* ((name (mbe :logic (str-fix name) :exec name))
         (syntax (mbe :logic (str-fix syntax)
                      :exec syntax))
         (date (mbe :logic (str-fix date) :exec date))
         (ltime (mbe :logic (nfix ltime) :exec ltime))
         (design (mbe :logic (vl-design-fix design)
                      :exec design))
         (filemap (mbe :logic (vl-filemap-fix filemap)
                       :exec filemap))
         (defines (mbe :logic (vl-defines-fix defines)
                       :exec defines)
))
      (cons :vl-zip (list (cons 'name name)
                          (cons 'syntax syntax)
                          (cons 'date date)
                          (cons 'ltime ltime)
                          (cons 'design design)
                          (cons 'filemap filemap)
                          (cons 'defines defines))))))