		Search-engine friendly clone of the ACL2 documentation.

Lint-warning-suppression

Vl-lint-scan-for-ignore

Signature
(vl-lint-scan-for-ignore x mwtype) → ignorep
Arguments: x — Arbitrary stuff that might occur in a warning's args.; mwtype — Guard (stringp mwtype).
Returns: ignorep — Type (booleanp ignorep).

Definitions and Theorems

Function: vl-lint-scan-for-ignore

(defun vl-lint-scan-for-ignore (x mwtype)
 (declare (xargs :guard (stringp mwtype)))
 (let ((__function__ 'vl-lint-scan-for-ignore))
  (declare (ignorable __function__))
  (b*
   (((when (atom x)) nil)
    ((when (symbolp (car x)))
     (if (eq (car x) :vl-module)
         nil
      (case
       (car x)
       ((:vl-special :vl-literal :vl-index
                     :vl-unary :vl-binary
                     :vl-qmark :vl-mintypmax
                     :vl-concat :vl-multiconcat
                     :vl-stream :vl-call
                     :vl-cast :vl-inside
                     :vl-tagged :vl-pattern)
        (and (vl-expr-p x)
             (vl-expr-scan-for-ignore x mwtype)))
       (:vl-assign (and (vl-assign-p x)
                        (vl-assign-scan-for-ignore x mwtype)))
       (:vl-modinst (and (vl-modinst-p x)
                         (vl-modinst-scan-for-ignore x mwtype)))
       (:vl-gateinst (and (vl-gateinst-p x)
                          (vl-gateinst-scan-for-ignore x mwtype)))
       (:vl-portdecl (and (vl-portdecl-p x)
                          (vl-portdecl-scan-for-ignore x mwtype)))
       (:vl-vardecl (and (vl-vardecl-p x)
                         (vl-vardecl-scan-for-ignore x mwtype)))
       (:vl-paramdecl (and (vl-paramdecl-p x)
                           (vl-paramdecl-scan-for-ignore x mwtype)))
       (:vl-fundecl (and (vl-fundecl-p x)
                         (vl-fundecl-scan-for-ignore x mwtype)))
       (:vl-taskdecl (and (vl-taskdecl-p x)
                          (vl-taskdecl-scan-for-ignore x mwtype)))
       (:vl-always (and (vl-always-p x)
                        (vl-always-scan-for-ignore x mwtype)))
       (:vl-initial (and (vl-initial-p x)
                         (vl-initial-scan-for-ignore x mwtype)))
       (:vl-plainarg (and (vl-plainarg-p x)
                          (vl-plainarg-scan-for-ignore x mwtype)))
       (:vl-namedarg (and (vl-namedarg-p x)
                          (vl-namedarg-scan-for-ignore x mwtype)))
       (:vl-context (and (vl-context1-p x)
                         (vl-context1-scan-for-ignore x mwtype)))
       ((:vl-nullstmt :vl-assignstmt :vl-deassignstmt
                      :vl-callstmt :vl-disablestmt
                      :vl-eventtriggerstmt :vl-casestmt
                      :vl-ifstmt :vl-foreverstmt
                      :vl-waitstmt :vl-repeatstmt
                      :vl-whilestmt :vl-forstmt
                      :vl-foreachstmt :vl-breakstmt
                      :vl-continuestmt :vl-blockstmt
                      :vl-timingstmt :vl-returnstmt
                      :vl-assertstmt :vl-cassertstmt)
        (and (vl-stmt-p x)
             (vl-stmt-scan-for-ignore x mwtype)))
       (otherwise nil)))))
   (or (vl-lint-scan-for-ignore (car x) mwtype)
       (vl-lint-scan-for-ignore (cdr x)
                                mwtype)))))

Theorem: booleanp-of-vl-lint-scan-for-ignore

(defthm booleanp-of-vl-lint-scan-for-ignore
  (b* ((ignorep (vl-lint-scan-for-ignore x mwtype)))
    (booleanp ignorep))
  :rule-classes :type-prescription)