• Top
    • Documentation
    • Books
    • Recursion-and-induction
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
      • Gl
      • Esim
      • Vl2014
        • Warnings
          • Vl-warninglist->types
          • Vl-warning
          • Propagating-errors
          • Vl-reportcard
          • Vl-warning-sort
          • Lint-warning-suppression
          • Clean-warnings
          • Warn
            • Vl-some-warning-fatalp
            • Vl-print-warnings-with-header
            • Vl-print-warnings-with-named-header
            • Flat-warnings
            • Vl-keep-warnings
            • Vl-remove-warnings
            • Vl-print-warnings
            • Vl-some-warning-of-type-p
            • Vl-clean-warnings
            • Vl-warnings-to-string
            • Vl-warninglist
            • Vl-print-warning
            • Ok
            • Vl-trace-warnings
            • Fatal
          • Primitives
          • Use-set
          • Syntax
          • Getting-started
          • Utilities
          • Loader
          • Transforms
          • Lint
          • Mlib
          • Server
          • Kit
          • Printer
          • Esim-vl
          • Well-formedness
        • Sv
        • Vwsim
        • Fgl
        • Vl
        • X86isa
        • Svl
        • Rtl
      • Software-verification
      • Testing-utilities
      • Math
    • Warnings

    Warn

    Extend a warnings accumulator with a non-fatal warning.

    Syntax:

    (warn [:type type]
          [:msg msg]
          [:args args]
          [:fn fn]         ;; defaults to __function__
          [:acc warnings]  ;; defaults to warnings
          )
       -->
    warnings'

    This macro builds a new, non-fatal warning w from the given type, msg, args, and fn, then conses w onto the warnings accumulator acc.

    See also fatal; it is identical except that it builds fatal warnings.

    We make use of a few interfacing tricks:

    • acc defaults to warnings because we often use warnings as the name of the warnings accumulator we are working with. That is, as long as your warnings accumulator is named warnings, you don't have to give an acc argument.
    • fn defaults to __function__. Macros like define often bind this symbol to the name of the current function, so if you are using a macro like this you don't have to give a fn argument. But you will need to explicitly give a function name when using raw defun.
    • We cons the new warning not onto acc, but instead onto (vl-warninglist-fix acc). This ensures that code written using warn can unconditionally produce vl-warninglist-ps, without needing to do explicit fixing.