		Search-engine friendly clone of the ACL2 documentation.
Vl-lint
Vl-lint-top

Top-level vl lint command.
Signature
(vl-lint-top args &key (state 'state)) → state
Arguments: args — Guard (string-listp args).
Definitions and Theorems

Function: vl-lint-top-fn
(defun vl-lint-top-fn (args state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (string-listp args)))
 (let ((__function__ 'vl-lint-top))
  (declare (ignorable __function__))
  (b*
   (((mv errmsg config start-files-and-plusargs)
     (parse-vl-lintconfig args))
    ((when errmsg)
     (die "~@0~%" errmsg)
     state)
    ((mv start-files plusargs)
     (split-plusargs start-files-and-plusargs))
    (config (change-vl-lintconfig config
                                  :plusargs plusargs
                                  :start-files start-files))
    ((vl-lintconfig config) config)
    (- (set-max-mem (* (expt 2 30) config.mem)))
    (- (set-vl-gc-threshold (floor (* 6 (expt 2 30) config.mem)
                                   10)))
    (- (set-vl-gc-baseline))
    ((when config.help)
     (vl-cw-ps-seq (vl-print *vl-lint-help*))
     (exit-ok)
     state)
    ((when config.readme)
     (vl-cw-ps-seq (vl-print *vl-lint-readme*))
     (exit-ok)
     state)
    (- (or (not config.debug)
           (vl-cw-ps-seq (vl-cw "Raw args: ~x0~%" args)
                         (vl-cw "Start-files: ~x0~%" start-files))))
    ((unless (consp config.start-files))
     (die "No files to process.")
     state)
    (state (must-be-regular-files! config.start-files))
    (state (must-be-directories! config.search-path))
    (state (must-be-directories! config.include-dirs))
    ((when config.shell)
     (vl-shell-entry
          (cons (cons 'defconst
                      (cons '*vl-user-lintconfig*
                            (cons (cons 'quote (cons config 'nil))
                                  'nil)))
                'nil)))
    ((mv result loadres loadconfig state)
     (cwtime (run-vl-lint config)
             :name vl-lint))
    (state (cwtime (vl-lint-report config loadres result state)))
    ((when config.post-shell)
     (b* ((print (and (boundp-global 'ld-pre-eval-print state)
                      (f-get-global 'ld-pre-eval-print
                                    state))))
      (vl-shell-entry
       (cons
        '(set-ld-pre-eval-print nil state)
        (cons
         (cons 'defconst
               (cons '*vl-user-lintconfig*
                     (cons (cons 'quote (cons config 'nil))
                           'nil)))
         (cons
          (cons 'defconst
                (cons '*vl-user-loadconfig*
                      (cons (cons 'quote (cons loadconfig 'nil))
                            'nil)))
          (cons
           (cons 'defconst
                 (cons '*vl-user-loadres*
                       (cons (cons 'quote (cons loadres 'nil))
                             'nil)))
           (cons
            '(defconst *vl-user-design*
               (vl-loadresult->design *vl-user-loadres*))
            (cons (cons 'defconst
                        (cons '*vl-user-lintresult*
                              (cons (cons 'quote (cons result 'nil))
                                    'nil)))
                  (cons (cons 'set-ld-pre-eval-print
                              (cons (cons 'quote (cons print 'nil))
                                    '(state)))
                        'nil)))))))))))
   (exit-ok)
   state)))