• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Community
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
      • Gl
      • Esim
      • Vl2014
      • Sv
      • Fgl
      • Vwsim
      • Vl
        • Syntax
        • Loader
        • Warnings
          • Lint-warning-suppression
          • Warning-basics
          • Vl-warning
          • Vl-warninglist-add-ctx
          • Vl-warninglist->types
          • Propagating-errors
          • Vl-reportcard
          • Vl-some-warning-fatalp
          • Clean-warnings
          • Lint-whole-file-suppression
          • Warn
          • Vl-warninglist
            • Vl-warninglist-p
            • Vl-warninglist-fix
            • Vl-print-warnings-with-header
              • Vl-warninglist-equiv
              • Vl-print-warnings-with-named-header
              • Vl-print-warnings
              • Vl-warnings-to-string
            • Vl-remove-warnings
            • Vl-keep-warnings
            • Flat-warnings
            • Vl-some-warning-of-type-p
            • Vl-msg
            • Vl-warning-add-ctx
            • Vl-print-warning
            • Vmsg-binary-concat
            • Ok
            • Vl-trace-warnings
            • Fatal
            • Vmsg
          • Getting-started
          • Utilities
          • Printer
          • Kit
          • Mlib
          • Transforms
        • X86isa
        • Svl
        • Rtl
      • Software-verification
      • Math
      • Testing-utilities
    • Vl-warninglist

    Vl-print-warnings-with-header

    Pretty-print a vl-warninglist with a header saying how many warnings there are.

    Signature
    (vl-print-warnings-with-header x &key (ps 'ps)) → ps
    Arguments
    x — Guard (vl-warninglist-p x).

    This is almost identical to vl-print-warnings, but it also prefaces the list of warnings with a header that says how many warnings there are. Also, whereas vl-print-warnings is essentially invisible if there are no warnings, in such cases this function at least prints "No warnings".

    Definitions and Theorems

    Function: vl-print-warnings-with-header-fn

    (defun vl-print-warnings-with-header-fn (x ps)
     (declare (xargs :stobjs (ps)))
     (declare (xargs :guard (vl-warninglist-p x)))
     (let ((__function__ 'vl-print-warnings-with-header))
      (declare (ignorable __function__))
      (b* ((htmlp (vl-ps->htmlp))
           (x (vl-clean-warnings x))
           (msg (cond ((atom x) "No Warnings")
                      ((atom (cdr x)) "One Warning")
                      (t (cat (natstr (len x)) " Warnings")))))
       (if (not htmlp)
           (vl-ps-seq (vl-println msg)
                      (vl-print-warnings-aux x))
        (vl-ps-seq
         (vl-println-markup "<div class=\"vl_module_warnings\">")
         (if (atom x)
             (vl-print-markup "<h3 class=\"vl_module_no_warnings\">")
           (vl-print-markup "<h3 class=\"vl_module_yes_warnings\">"))
         (vl-print msg)
         (vl-println-markup "</h3>")
         (if (atom x)
             ps
           (vl-ps-seq (vl-println-markup "<ul class=\"vl_warning_list\">")
                      (vl-print-warnings-aux x)
                      (vl-println-markup "</ul>")))
         (vl-println-markup "</div>"))))))

    Theorem: vl-print-warnings-with-header-fn-of-vl-warninglist-fix-x

    (defthm vl-print-warnings-with-header-fn-of-vl-warninglist-fix-x
      (equal (vl-print-warnings-with-header-fn (vl-warninglist-fix x)
                                               ps)
             (vl-print-warnings-with-header-fn x ps)))

    Theorem: vl-print-warnings-with-header-fn-vl-warninglist-equiv-congruence-on-x

    (defthm
     vl-print-warnings-with-header-fn-vl-warninglist-equiv-congruence-on-x
     (implies (vl-warninglist-equiv x x-equiv)
              (equal (vl-print-warnings-with-header-fn x ps)
                     (vl-print-warnings-with-header-fn x-equiv ps)))
     :rule-classes :congruence)