• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Community
    • 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
        • Fgl
        • Vwsim
        • Vl
        • X86isa
        • Svl
        • Rtl
      • Software-verification
      • Math
      • Testing-utilities
    • Lint-warning-suppression

    Vl-mash-warning-string

    Do basic string mashing to allow the user to refer to warnings in either upper or lower case, treating - and _ as equivalent, and with or without vl_warn_ prefixes.

    Signature
    (vl-mash-warning-string x) → new-x
    Arguments
    x — Guard (stringp x).
    Returns
    new-x — Type (stringp new-x).

    Definitions and Theorems

    Function: vl-mash-warning-string

    (defun vl-mash-warning-string (x)
      (declare (xargs :guard (stringp x)))
      (let ((__function__ 'vl-mash-warning-string))
        (declare (ignorable __function__))
        (b* ((x (str::upcase-string x))
             (x (str::strsubst "-" "_" x))
             (x (if (str::strprefixp "_" x)
                    (subseq x 1 nil)
                  x))
             (x (if (str::strprefixp "VL_" x)
                    (ec-call (subseq x 3 nil))
                  x))
             (x (if (str::strprefixp "WARN_" x)
                    (ec-call (subseq x 5 nil))
                  x)))
          x)))

    Theorem: stringp-of-vl-mash-warning-string

    (defthm stringp-of-vl-mash-warning-string
      (b* ((new-x (vl-mash-warning-string x)))
        (stringp new-x))
      :rule-classes :type-prescription)

    Theorem: vl-mash-warning-string-of-str-fix-x

    (defthm vl-mash-warning-string-of-str-fix-x
      (equal (vl-mash-warning-string (str-fix x))
             (vl-mash-warning-string x)))

    Theorem: vl-mash-warning-string-streqv-congruence-on-x

    (defthm vl-mash-warning-string-streqv-congruence-on-x
      (implies (streqv x x-equiv)
               (equal (vl-mash-warning-string x)
                      (vl-mash-warning-string x-equiv)))
      :rule-classes :congruence)