• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Debugging
  • Projects
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
      • Warnings
      • Primitives
      • Use-set
      • Syntax
      • Getting-started
      • Utilities
      • Loader
      • Transforms
      • Lint
        • Vl-lintconfig-p
        • Lucid
        • Skip-detection
        • Vl-lintresult-p
        • Lint-warning-suppression
          • Vl-mash-warning-strings
          • Vl-design-lint-ignoreall
          • Vl-design-suppress-lint-warnings
          • Vl-warninglist-lint-ignoreall
          • Vl-lint-scan-for-ignore
          • Vl-mash-warning-string
          • Vl-lint-suppress-warnings
          • Vl-warning-type-mash
          • Vl-lint-ignore-att-p
          • Vl-lint-atts-say-ignore
          • Vl-lint-attname-says-ignore
          • Vl-lint-ignore-att-mash
        • Condcheck
        • Selfassigns
        • Leftright-check
        • Dupeinst-check
        • Oddexpr-check
        • Remove-toohard
        • Qmarksize-check
        • Portcheck
        • Duplicate-detect
        • Vl-print-certain-warnings
        • Duperhs-check
        • *vl-lint-help*
        • Lint-stmt-rewrite
        • Drop-missing-submodules
        • Check-case
        • Drop-user-submodules
        • Check-namespace
        • Vl-lint
      • Mlib
      • Server
      • Kit
      • Printer
      • Esim-vl
      • Well-formedness
    • Sv
    • Vwsim
    • Fgl
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• 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
      (or
       (case
        (car x)
        (:nonatom (and (vl-expr-p x)
                       (eq (vl-expr-kind x) :nonatom)
                       (vl-lint-atts-say-ignore (vl-nonatom->atts x)
                                                mwtype)))
        (:vl-assign
             (and (vl-assign-p x)
                  (vl-lint-atts-say-ignore (vl-assign->atts x)
                                           mwtype)))
        (:vl-modinst
             (and (vl-modinst-p x)
                  (vl-lint-atts-say-ignore (vl-modinst->atts x)
                                           mwtype)))
        (:vl-gateinst
             (and (vl-gateinst-p x)
                  (vl-lint-atts-say-ignore (vl-gateinst->atts x)
                                           mwtype)))
        (:vl-portdecl
             (and (vl-portdecl-p x)
                  (vl-lint-atts-say-ignore (vl-portdecl->atts x)
                                           mwtype)))
        (:vl-vardecl
             (and (vl-vardecl-p x)
                  (vl-lint-atts-say-ignore (vl-vardecl->atts x)
                                           mwtype)))
        (:vl-paramdecl
             (and (vl-paramdecl-p x)
                  (vl-lint-atts-say-ignore (vl-paramdecl->atts x)
                                           mwtype)))
        (:vl-fundecl
             (and (vl-fundecl-p x)
                  (vl-lint-atts-say-ignore (vl-fundecl->atts x)
                                           mwtype)))
        (:vl-taskdecl
             (and (vl-taskdecl-p x)
                  (vl-lint-atts-say-ignore (vl-taskdecl->atts x)
                                           mwtype)))
        (:vl-always
             (and (vl-always-p x)
                  (vl-lint-atts-say-ignore (vl-always->atts x)
                                           mwtype)))
        (:vl-initial
             (and (vl-initial-p x)
                  (vl-lint-atts-say-ignore (vl-initial->atts x)
                                           mwtype)))
        (:vl-plainarg
             (and (vl-plainarg-p x)
                  (vl-lint-atts-say-ignore (vl-plainarg->atts x)
                                           mwtype)))
        (:vl-namedarg
             (and (vl-namedarg-p x)
                  (vl-lint-atts-say-ignore (vl-namedarg->atts x)
                                           mwtype)))
        ((:vl-nullstmt :vl-assignstmt :vl-deassignstmt
                       :vl-enablestmt :vl-disablestmt
                       :vl-eventtriggerstmt :vl-casestmt
                       :vl-ifstmt :vl-foreverstmt
                       :vl-waitstmt :vl-whilestmt
                       :vl-forstmt :vl-blockstmt
                       :vl-repeatstmt :vl-timingstmt)
         (and (vl-stmt-p x)
              (vl-lint-atts-say-ignore (vl-stmt->atts x)
                                       mwtype)))
        (otherwise nil))
       (vl-lint-scan-for-ignore (cdr x)
                                mwtype)))))
   (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)