• 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

    Pretty-print a vl-warninglist.

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

    We automatically clean the warnings; see vl-clean-warnings.

    Note that no header information is printed, this just prints the list of warnings.

    See also vl-print-warnings-with-header and vl-warnings-to-string.

    Definitions and Theorems

    Function: vl-print-warnings-fn

    (defun vl-print-warnings-fn (x ps)
     (declare (xargs :stobjs (ps)))
     (declare (xargs :guard (vl-warninglist-p x)))
     (let ((__function__ 'vl-print-warnings))
      (declare (ignorable __function__))
      (let* ((htmlp (vl-ps->htmlp))
             (x (vl-clean-warnings x)))
       (cond
        ((not htmlp) (vl-print-warnings-aux x))
        ((atom x) ps)
        (t (vl-ps-seq (vl-println-markup "<ul class=\"vl_warning_list\">")
                      (vl-print-warnings-aux x)
                      (vl-println-markup "</ul>")))))))

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

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

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

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