		Search-engine friendly clone of the ACL2 documentation.

Vl-lint

Vl-module-add-svbad-warnings

Signature
(vl-module-add-svbad-warnings x good bad) → (mv good bad)
Arguments: x — Guard (vl-module-p x).; good — Guard (vl-modulelist-p good).; bad — Guard (vl-modulelist-p bad).
Returns: good — Type (vl-modulelist-p good).; bad — Type (vl-modulelist-p bad).

Definitions and Theorems

Function: vl-module-add-svbad-warnings

(defun vl-module-add-svbad-warnings (x good bad)
 (declare (xargs :guard (and (vl-module-p x)
                             (vl-modulelist-p good)
                             (vl-modulelist-p bad))))
 (let ((__function__ 'vl-module-add-svbad-warnings))
  (declare (ignorable __function__))
  (b*
   (((vl-module x) (vl-module-fix x))
    (good (vl-modulelist-fix good))
    (bad (vl-modulelist-fix bad))
    (warnings (vl-vardecllist-svbad-warnings x.vardecls nil))
    ((unless warnings)
     (mv (cons x good) bad))
    (new-x
        (change-vl-module
             x
             :warnings (append-without-guard warnings x.warnings))))
   (mv good (cons new-x bad)))))

Theorem: vl-modulelist-p-of-vl-module-add-svbad-warnings.good

(defthm vl-modulelist-p-of-vl-module-add-svbad-warnings.good
  (b* (((mv ?good ?bad)
        (vl-module-add-svbad-warnings x good bad)))
    (vl-modulelist-p good))
  :rule-classes :rewrite)

Theorem: vl-modulelist-p-of-vl-module-add-svbad-warnings.bad

(defthm vl-modulelist-p-of-vl-module-add-svbad-warnings.bad
  (b* (((mv ?good ?bad)
        (vl-module-add-svbad-warnings x good bad)))
    (vl-modulelist-p bad))
  :rule-classes :rewrite)