• 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
          • Preprocessor
          • Vl-loadconfig
          • Lexer
          • Vl-loadstate
            • Vl-loadstate-fix
            • Vl-loadstate-p
            • Make-vl-loadstate
            • Vl-loadstate-equiv
            • Change-vl-loadstate
            • Vl-loadstate->reportcard
            • Vl-loadstate->descalist
            • Vl-loadstate->pstate
            • Vl-loadstate->filemap
            • Vl-loadstate->descs
            • Vl-loadstate->defines
            • Vl-loadstate->config
          • Parser
          • Vl-load-merge-descriptions
          • Scope-of-defines
          • Vl-load-file
          • Vl-flush-out-descriptions
          • Vl-description
          • Vl-loadresult
          • Vl-read-file
          • Vl-find-basename/extension
          • Vl-find-file
          • Vl-read-files
          • Extended-characters
          • Vl-load
          • Vl-load-main
          • Vl-load-description
          • Vl-descriptions-left-to-load
          • Inject-warnings
          • Vl-load-descriptions
          • Vl-load-files
          • Vl-load-summary
          • Vl-collect-modules-from-descriptions
          • Vl-descriptionlist
        • Transforms
        • Lint
        • Mlib
        • Server
        • Kit
        • Printer
        • Esim-vl
        • Well-formedness
      • Sv
      • Fgl
      • Vwsim
      • Vl
      • X86isa
      • Svl
      • Rtl
    • Software-verification
    • Math
    • Testing-utilities
  • Loader

Vl-loadstate

Internal state object used throughout the VL loading routines.

This is a product type introduced by defprod.

Fields
config — vl-loadconfig
Original configuration passed to vl-load. This remains constant throughout our loading routines.
descs — vl-descriptionlist
Top-level descriptions (modules, packages, interfaces, etc.) we have loaded so far. These descriptions have been only minimally transformed, and are intended to capture the actual source code in the files on disk.
descalist
Fast alist of description names, for fast lookups.
defines — vl-defines
The current set of `defines at any point in time.
reportcard — vl-reportcard
Main storage for load-time warnings that we want to associate with particular descriptions. This is where most load-time warnings from loading are kept during loading. At the end of loading, these warnings get injected into the actual descriptions they pertain to.
pstate — vl-parsestate
State that the parser needs. BOZO probably we should consider moving some of the loadstate into the pstate. This holds, among other things, any "floating" warnings that aren't associated with any description. But few warnings get put here. Instead, most warnings get associated with particular descriptions. But some warnings from the early stages of file loading (like preprocessing and lexing), or warnings about malformed syntax that occurs between descriptions, can end up here.
filemap — vl-filemap
Database mapping the names of files we have read to their contents. This is occasionally useful for seeing the original code for a description. To save memory, you can avoid constructing this alist; see the filemapp option in vl-loadconfig-p.
Additional Requirements

The following invariant is enforced on the fields:

(equal descalist (vl-make-descalist descs))

Subtopics

Vl-loadstate-fix
Fixing function for vl-loadstate structures.
Vl-loadstate-p
Recognizer for vl-loadstate structures.
Make-vl-loadstate
Basic constructor macro for vl-loadstate structures.
Vl-loadstate-equiv
Basic equivalence relation for vl-loadstate structures.
Change-vl-loadstate
Modifying constructor for vl-loadstate structures.
Vl-loadstate->reportcard
Get the reportcard field from a vl-loadstate.
Vl-loadstate->descalist
Get the descalist field from a vl-loadstate.
Vl-loadstate->pstate
Get the pstate field from a vl-loadstate.
Vl-loadstate->filemap
Get the filemap field from a vl-loadstate.
Vl-loadstate->descs
Get the descs field from a vl-loadstate.
Vl-loadstate->defines
Get the defines field from a vl-loadstate.
Vl-loadstate->config
Get the config field from a vl-loadstate.