		Search-engine friendly clone of the ACL2 documentation.

Vl-lint

The vl lint command.

Signature
(vl-lint args &key (state 'state)) → state
Arguments: args — Guard (string-listp args).

Definitions and Theorems

Function: vl-lint-fn

(defun vl-lint-fn (args state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (string-listp args)))
 (let ((__function__ 'vl-lint))
  (declare (ignorable __function__))
  (b*
   (((mv errmsg config start-files)
     (parse-vl-lintconfig args))
    ((when errmsg)
     (die "~@0~%" errmsg)
     state)
    (config (change-vl-lintconfig config
                                  :start-files start-files))
    ((vl-lintconfig config) config)
    (- (acl2::set-max-mem (* (expt 2 30) config.mem)))
    ((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))
    ((mv result state)
     (cwtime (run-vl-lint config)
             :name vl-lint))
    (state (cwtime (vl-lint-report result state))))
   (exit-ok)
   state)))