		Search-engine friendly clone of the ACL2 documentation.

Vl-lint

Run-vl-lint

Signature
(run-vl-lint config &key (state 'state)) → (mv res loadres loadconfig state)
Arguments: config — Guard (vl-lintconfig-p config).
Returns: res — Type (vl-lintresult-p res).; loadres — Type (vl-loadresult-p loadres).; loadconfig — Type (vl-loadconfig-p loadconfig).; state — Type (state-p1 state), given (state-p1 state).

Definitions and Theorems

Function: run-vl-lint-fn

(defun run-vl-lint-fn (config state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (vl-lintconfig-p config)))
 (let ((__function__ 'run-vl-lint))
  (declare (ignorable __function__))
  (b*
   ((- (cw "Starting VL-Lint~%"))
    ((vl-lintconfig config) config)
    (- (or (not config.debug)
           (cw "Lint configuration: ~x0~%" config)))
    ((mv cmdline-warnings defines)
     (vl-parse-cmdline-defines
          config.defines
          (make-vl-location :filename "vl cmdline"
                            :line 1
                            :col 0)
          t))
    (- (or (not cmdline-warnings)
           (vl-cw-ps-seq (vl-print-warnings cmdline-warnings))))
    (loadconfig (vl-lintconfig-loadconfig config defines))
    (- (or (not config.debug)
           (cw "Load configuration: ~x0~%"
               loadconfig)))
    (- (cw "~%vl-lint: loading modules...~%"))
    ((mv loadres state)
     (cwtime (vl-load loadconfig)))
    (design (vl-loadresult->design loadres))
    (design
         (change-vl-design
              design
              :warnings
              (append-without-guard cmdline-warnings
                                    (vl-design->warnings design))))
    (lintres (cwtime (run-vl-lint-main design config)))
    (state
     (cwtime
         (vl-lint-extra-actions config
                                loadconfig loadres lintres state))))
   (mv lintres loadres loadconfig state))))

Theorem: vl-lintresult-p-of-run-vl-lint.res

(defthm vl-lintresult-p-of-run-vl-lint.res
  (b* (((mv ?res ?loadres ?loadconfig acl2::?state)
        (run-vl-lint-fn config state)))
    (vl-lintresult-p res))
  :rule-classes :rewrite)

Theorem: vl-loadresult-p-of-run-vl-lint.loadres

(defthm vl-loadresult-p-of-run-vl-lint.loadres
  (b* (((mv ?res ?loadres ?loadconfig acl2::?state)
        (run-vl-lint-fn config state)))
    (vl-loadresult-p loadres))
  :rule-classes :rewrite)

Theorem: vl-loadconfig-p-of-run-vl-lint.loadconfig

(defthm vl-loadconfig-p-of-run-vl-lint.loadconfig
  (b* (((mv ?res ?loadres ?loadconfig acl2::?state)
        (run-vl-lint-fn config state)))
    (vl-loadconfig-p loadconfig))
  :rule-classes :rewrite)

Theorem: state-p1-of-run-vl-lint.state

(defthm state-p1-of-run-vl-lint.state
  (implies (state-p1 state)
           (b* (((mv ?res ?loadres ?loadconfig acl2::?state)
                 (run-vl-lint-fn config state)))
             (state-p1 state)))
  :rule-classes :rewrite)