• 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
        • Mlib
          • Scopestack
          • Filtering-by-name
          • Vl-namefactory
          • Substitution
          • Allexprs
          • Hid-tools
          • Vl-consteval
          • Range-tools
          • Lvalexprs
          • Hierarchy
            • Vl-remove-unnecessary-elements
            • Vl-necessary-elements-transitive
            • Vl-dependent-elements-transitive
            • Vl-necessary-elements-direct
            • Vl-modulelist-everinstanced
            • Vl-dependent-elements-direct
            • Vl-modulelist-toplevel
            • Vl-design-deporder-modules
            • Vl-design-check-complete
            • Vl-design-upgraph
            • Immdeps
              • Immdeps-main
              • Vl-immdeps
                • Vl-immdeps-p
                • Vl-immdeps-add-error
                • Vl-immdeps-add-item
                • Vl-immdeps-add-definition
                • Vl-immdeps-add-pkgdep
                • Vl-immdeps-fix
                • Vl-immdeps-add-raw-dependency
                • Vl-immdeps-equiv
                • Make-vl-immdeps
                • Vl-immdeps->warnings
                • Vl-immdeps->deps
                • Vl-immdeps->all-okp
                • Change-vl-immdeps
              • Immdeps-top
              • Vl-immdepgraph
              • Vl-depgraph
            • Vl-design-downgraph
            • Vl-collect-dependencies
            • Vl-hierarchy-free
          • Finding-by-name
          • Expr-tools
          • Expr-slicing
          • Stripping-functions
          • Stmt-tools
          • Modnamespace
          • Vl-parse-expr-from-str
          • Welltyped
          • Reordering-by-name
          • Flat-warnings
          • Genblob
          • Expr-building
          • Datatype-tools
          • Syscalls
          • Relocate
          • Expr-cleaning
          • Namemangle
          • Caremask
          • Port-tools
          • Lvalues
        • Server
        • Kit
        • Printer
        • Esim-vl
        • Well-formedness
      • Sv
      • Fgl
      • Vwsim
      • Vl
      • X86isa
      • Svl
      • Rtl
    • Software-verification
    • Math
    • Testing-utilities
  • Immdeps

Vl-immdeps

Results of collecting up immediate dependencies.

This is a product type introduced by defprod.

Fields
all-okp — booleanp
Were we able to successfully resolve every identifier we encountered? Even when this is nil, we may be able to provide at least mostly accurate dependency information.
deps — string-listp
List of dependencies that have been collected. Note that for compatibility with depgraph::toposort, we exclude any dependencies that are not found as top-level design elements. For instance, if we find a module instance of module foo, but foo is not defined, we do not include a dependency on foo.
warnings — vl-warninglist
Any warnings accumulated during the process of collecting these dependencies.

It might be better to turn deps into a fast association list binding names we've seen to T, since there will likely be many duplicates. But, for now, we'll just use a simple list-based version. It would be easy to change this: just modify vl-immdeps-add-raw-dependency and vl-immdepgraph-merge.

Subtopics

Vl-immdeps-p
Recognizer for vl-immdeps structures.
Vl-immdeps-add-error
Note that there is an error with the dependencies we're collecting.
Vl-immdeps-add-item
Safely add a dependency onto an item (i.e., a parameter, variable, function name, type name, etc.)
Vl-immdeps-add-definition
Safely add a dependency onto a definition (i.e., an interface, module, user-defined primitive, etc. If there is no such definition, add a warning instead of a dependency.
Vl-immdeps-add-pkgdep
Safely add a dependency onto a package. If the package doesn't exist, add a warning instead of a dependency.
Vl-immdeps-fix
Fixing function for vl-immdeps structures.
Vl-immdeps-add-raw-dependency
Add a single top-level dependency to the answer we're building.
Vl-immdeps-equiv
Basic equivalence relation for vl-immdeps structures.
Make-vl-immdeps
Basic constructor macro for vl-immdeps structures.
Vl-immdeps->warnings
Get the warnings field from a vl-immdeps.
Vl-immdeps->deps
Get the deps field from a vl-immdeps.
Vl-immdeps->all-okp
Get the all-okp field from a vl-immdeps.
Change-vl-immdeps
Modifying constructor for vl-immdeps structures.