• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
      • Warnings
      • Primitives
      • Use-set
      • Syntax
      • Getting-started
      • Utilities
      • Loader
      • Transforms
      • Lint
        • Vl-lintconfig-p
          • Parse-vl-lintconfig
          • Vl-lintconfig
          • Make-vl-lintconfig
          • Change-vl-lintconfig
          • Honsed-vl-lintconfig
          • *vl-lintconfig-usage*
          • Make-honsed-vl-lintconfig
          • Vl-lintconfig->topmods
          • Vl-lintconfig->strict
          • Vl-lintconfig->start-files
          • Vl-lintconfig->search-path
          • Vl-lintconfig->search-exts
          • Vl-lintconfig->readme
          • Vl-lintconfig->quiet
          • Vl-lintconfig->mem
          • Vl-lintconfig->include-dirs
          • Vl-lintconfig->ignore
          • Vl-lintconfig->help
          • Vl-lintconfig->edition
          • Vl-lintconfig->dropmods
          • Vl-lintconfig->debug
          • Vl-lintconfig->cclimit
        • Lucid
        • Skip-detection
        • Vl-lintresult-p
        • Lint-warning-suppression
        • Condcheck
        • Selfassigns
        • Leftright-check
        • Dupeinst-check
        • Oddexpr-check
        • Remove-toohard
        • Qmarksize-check
        • Portcheck
        • Duplicate-detect
        • Vl-print-certain-warnings
        • Duperhs-check
        • *vl-lint-help*
        • Lint-stmt-rewrite
        • Drop-missing-submodules
        • Check-case
        • Drop-user-submodules
        • Check-namespace
        • Vl-lint
      • Mlib
      • Server
      • Kit
      • Printer
      • Esim-vl
      • Well-formedness
    • Sv
    • Fgl
    • Vwsim
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Vl-lintconfig-p

Honsed-vl-lintconfig

Raw constructor for honsed vl-lintconfig-p structures.

Syntax:

(honsed-vl-lintconfig start-files 
                      help readme search-path search-exts 
                      include-dirs topmods quiet dropmods 
                      ignore cclimit edition strict mem debug)

This is identical to vl-lintconfig, except that we hons the structure we are creating.

Definition

This is an ordinary honsing constructor introduced by defaggregate.

Function: honsed-vl-lintconfig

(defun honsed-vl-lintconfig
       (start-files help readme search-path search-exts
                    include-dirs topmods quiet dropmods
                    ignore cclimit edition strict mem debug)
 (declare (xargs :guard (and (string-listp start-files)
                             (booleanp help)
                             (booleanp readme)
                             (string-listp search-path)
                             (string-listp search-exts)
                             (string-listp include-dirs)
                             (string-listp topmods)
                             (string-listp quiet)
                             (string-listp dropmods)
                             (string-listp ignore)
                             (natp cclimit)
                             (vl-edition-p edition)
                             (booleanp strict)
                             (posp mem)
                             (booleanp debug))))
 (mbe
  :logic (vl-lintconfig start-files
                        help readme search-path search-exts
                        include-dirs topmods quiet dropmods
                        ignore cclimit edition strict mem debug)
  :exec
  (hons
   :vl-lint-opts
   (hons
    (hons 'start-files start-files)
    (hons
     (hons 'help help)
     (hons
      (hons 'readme readme)
      (hons
       (hons 'search-path search-path)
       (hons
        (hons 'search-exts search-exts)
        (hons
         (hons 'include-dirs include-dirs)
         (hons
          (hons 'topmods topmods)
          (hons
           (hons 'quiet quiet)
           (hons
            (hons 'dropmods dropmods)
            (hons
                 (hons 'ignore ignore)
                 (hons (hons 'cclimit cclimit)
                       (hons (hons 'edition edition)
                             (hons (hons 'strict strict)
                                   (hons (hons 'mem mem)
                                         (hons (hons 'debug debug)
                                               nil))))))))))))))))))