		Search-engine friendly clone of the ACL2 documentation.

Vl-lintresult

Results from running the linter.

This is a product type introduced by defprod.

design — vl-design: Final, transformed list of modules. Useful to know whether a module is unexpectedly included or not included.
design0 — vl-design: 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.
design-orig — vl-design: Really the initial, pre-transformed modules.
sv-modalist — sv::modalist: The result of converting the elaborated design into SV modules.
reportcard — vl-reportcard: The main result: binds "original" (pre-unparameterization) module names to their warnings.
sd-probs — sd-problemlist: Possible problems noticed by skip-detection. These are in a different format than ordinary warnings, so they aren't included in the reportcard.

Vl-lintresult-fix: Fixing function for vl-lintresult structures.
Make-vl-lintresult: Basic constructor macro for vl-lintresult structures.
Vl-lintresult-equiv: Basic equivalence relation for vl-lintresult structures.
Vl-lintresult-p: Recognizer for vl-lintresult structures.
Vl-lintresult->sv-modalist: Get the sv-modalist field from a vl-lintresult.
Vl-lintresult->sd-probs: Get the sd-probs field from a vl-lintresult.
Vl-lintresult->reportcard: Get the reportcard field from a vl-lintresult.
Vl-lintresult->design-orig: Get the design-orig field from a vl-lintresult.
Change-vl-lintresult: Modifying constructor for vl-lintresult structures.
Vl-lintresult->design0: Get the design0 field from a vl-lintresult.
Vl-lintresult->design: Get the design field from a vl-lintresult.