• 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

    Vl-lintconfig

    Raw constructor for vl-lintconfig-p structures.

    Syntax:

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

    This is the lowest-level constructor for vl-lintconfig-p structures. It simply conses together a structure with the specified fields.

    Note: It's generally better to use macros like make-vl-lintconfig or change-vl-lintconfig instead. These macros lead to more readable and robust code, because you don't have to remember the order of the fields.

    The vl-lintconfig-p structures we create here are just constructed with ordinary cons. If you want to create honsed structures, see honsed-vl-lintconfig instead.

    Definition

    This is an ordinary constructor function introduced by defaggregate.

    Function: vl-lintconfig

    (defun 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))))
     (cons
      :vl-lint-opts
      (cons
       (cons 'start-files start-files)
       (cons
        (cons 'help help)
        (cons
         (cons 'readme readme)
         (cons
          (cons 'search-path search-path)
          (cons
           (cons 'search-exts search-exts)
           (cons
            (cons 'include-dirs include-dirs)
            (cons
             (cons 'topmods topmods)
             (cons
              (cons 'quiet quiet)
              (cons
                (cons 'dropmods dropmods)
                (cons (cons 'ignore ignore)
                      (cons (cons 'cclimit cclimit)
                            (cons (cons 'edition edition)
                                  (cons (cons 'strict strict)
                                        (cons (cons 'mem mem)
                                              (cons (cons 'debug debug)
                                                    nil)))))))))))))))))