• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • 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
            • Vl-lintresult
            • Make-vl-lintresult
            • Change-vl-lintresult
            • Honsed-vl-lintresult
            • Make-honsed-vl-lintresult
            • Vl-lintresult->sd-probs
            • Vl-lintresult->reportcard
            • Vl-lintresult->design0
            • Vl-lintresult->design
          • Lint-warning-suppression
          • 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

Vl-lintresult-p

Results from running the linter.

(vl-lintresult-p x) is a defaggregate of the following fields.

  • design — Final, transformed list of modules. Typically this isn't very interesting or relevant to anything.
        Invariant (vl-design-p design).
  • design0 — Almost: the initial, pre-transformed modules. The only twist is that we have already removed modules that are unnecessary or that we wanted to drop; see, e.g., the topmods and ignore options of vl-lintconfig-p. This is used for skip-detection, for instance.
        Invariant (vl-design-p design0).
  • reportcard — The main result: binds "original" (pre-unparameterization) module names to their warnings.
        Invariant (vl-reportcard-p reportcard).
  • sd-probs — Possible problems noticed by skip-detection. These are in a different format than ordinary warnings, so they aren't included in the reportcard.
        Invariant (sd-problemlist-p sd-probs).

Source link: vl-lintresult-p

Subtopics

Vl-lintresult
Raw constructor for vl-lintresult-p structures.
Make-vl-lintresult
Constructor macro for vl-lintresult-p structures.
Change-vl-lintresult
A copying macro that lets you create new vl-lintresult-p structures, based on existing structures.
Honsed-vl-lintresult
Raw constructor for honsed vl-lintresult-p structures.
Make-honsed-vl-lintresult
Constructor macro for honsed vl-lintresult-p structures.
Vl-lintresult->sd-probs
Access the sd-probs field of a vl-lintresult-p structure.
Vl-lintresult->reportcard
Access the reportcard field of a vl-lintresult-p structure.
Vl-lintresult->design0
Access the design0 field of a vl-lintresult-p structure.
Vl-lintresult->design
Access the design field of a vl-lintresult-p structure.