		Search-engine friendly clone of the ACL2 documentation.

Vl-lint

Vl-lint-design->svex-modalist-wrapper

Signature
(vl-lint-design->svex-modalist-wrapper x config) → new-x
Arguments: x — Guard (vl-design-p x).; config — Guard (vl-simpconfig-p config).
Returns: new-x — Type (vl-design-p new-x).

Definitions and Theorems

Function: vl-lint-design->svex-modalist-wrapper

(defun vl-lint-design->svex-modalist-wrapper (x config)
 (declare (xargs :guard (and (vl-design-p x)
                             (vl-simpconfig-p config))))
 (let ((__function__ 'vl-lint-design->svex-modalist-wrapper))
  (declare (ignorable __function__))
  (b*
   (((vl-design x))
    (- (sneaky-save :vl-lint-svconfig config))
    (- (sneaky-save :vl-lint-pre-sv-design x))
    ((mv good bad)
     (vl-modulelist-add-svbad-warnings x.mods nil nil))
    (good-x (change-vl-design x :mods good))
    ((mv reportcard ?modalist)
     (xf-cwtime (vl-design->svex-modalist good-x
                                          :config config)))
    (merged-x
         (change-vl-design x
                           :mods (append-without-guard good bad)))
    (final-x (xf-cwtime (vl-apply-reportcard merged-x reportcard))))
   final-x)))

Theorem: vl-design-p-of-vl-lint-design->svex-modalist-wrapper

(defthm vl-design-p-of-vl-lint-design->svex-modalist-wrapper
  (b* ((new-x (vl-lint-design->svex-modalist-wrapper x config)))
    (vl-design-p new-x))
  :rule-classes :rewrite)