• Top
    • Documentation
    • Books
    • Recursion-and-induction
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
      • Gl
      • Esim
      • Vl2014
      • Sv
      • Vwsim
      • Fgl
      • Vl
        • Syntax
        • Loader
          • Preprocessor
          • Vl-loadconfig
          • Vl-loadstate
          • Lexer
          • Parser
          • Vl-load-merge-descriptions
          • Vl-find-basename/extension
          • Vl-load-file
          • Vl-loadresult
          • Vl-find-file
          • Scope-of-defines
          • Vl-flush-out-descriptions
          • Vl-description
          • Vl-read-file
          • Vl-includeskips-report-gather
          • Vl-load-main
          • Extended-characters
          • Vl-load
          • Vl-load-description
          • Vl-preprocess-debug
          • Vl-descriptions-left-to-load
          • Inject-warnings
            • Vl-filter-warnings-by-loc
            • Vl-descriptionlist-inject-warnings
            • Vl-description-inject-warnings
            • Vl-description-add-warnings
            • Vl-warning->loc
          • Vl-read-file-report-gather
          • Vl-write-preprocessor-debug-file
          • Vl-load-descriptions
          • Vl-load-files
          • Translate-off
          • Vl-load-read-file-hook
          • Vl-loadstate-pad
          • Vl-read-file-report
          • Vl-load-summary
          • Vl-collect-modules-from-descriptions
          • Vl-loadstate->warnings
          • Vl-iskips-report
          • Vl-descriptionlist
        • Warnings
        • Getting-started
        • Utilities
        • Printer
        • Kit
        • Mlib
        • Transforms
      • X86isa
      • Svl
      • Rtl
    • Software-verification
    • Testing-utilities
    • Math
  • Loader

Inject-warnings

Mechanism for attaching warnings to particular modules or other design elements.

Warnings from the early stages of parsing (e.g., lexing and preprocessing) are created well before we have any modules (or other kinds of descriptions, e.g., interfaces) to attach them to. By convention, we create these warnings so that their first argument is the location. When warnings follow this convention, we can attempt to associate them with modules.

Note: we generally don't expect there to be too many warnings caused during these stages of loading, so our injection code is not particularly efficient.

Subtopics

Vl-filter-warnings-by-loc
Extract warnings that are between certain bounds.
Vl-descriptionlist-inject-warnings
Extract and attach in-bounds warnings to a description list.
Vl-description-inject-warnings
Extract and attach in-bounds warnings to a description.
Vl-description-add-warnings
Add a list of warnings to a (suitable) description.
Vl-warning->loc
Return the location of a warning, if it obeys the location convention.