• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
      • Kestrel-books
        • Crypto-hdwallet
        • Apt
        • Error-checking
        • Fty-extensions
        • Isar
        • Kestrel-utilities
        • Set
        • Soft
        • C
          • Syntax-for-tools
            • Disambiguator
            • Abstract-syntax
            • Parser
            • Validator
            • Printer
            • Formalized-subset
            • Mapping-to-language-definition
            • Input-files
            • Defpred
            • Output-files
            • Abstract-syntax-operations
            • Validation-information
              • Abstract-syntax-annop
              • Types
              • Valid-ord-info
              • Lifetime
              • Valid-defstatus
              • Valid-table
              • Valid-ord-info-option
              • Linkage-option
              • Linkage
              • Lifetime-option
              • Iconst-info
              • Var-info
              • Valid-scope
              • Stmt-type
              • Expr-null-pointer-constp
              • Transunit-info
                • Transunit-info-fix
                • Transunit-info-equiv
                • Make-transunit-info
                • Transunit-info->table
                • Change-transunit-info
                • Transunit-infop
              • Expr-type
              • Const-expr-null-pointer-constp
              • Unary-info
              • Binary-info
              • Block-item-list-type
              • Block-item-type
              • Valid-ord-scope
              • Coerce-transunit-info
              • Coerce-var-info
              • Coerce-unary-info
              • Coerce-iconst-info
              • Coerce-binary-info
              • Irr-transunit-info
              • Irr-iconst-info
              • Irr-binary-info
              • Irr-var-info
              • Irr-valid-table
              • Irr-unary-info
              • Valid-scope-list
              • Irr-linkage
              • Irr-lifetime
            • Implementation-environments
            • Concrete-syntax
            • Unambiguity
            • Ascii-identifiers
            • Preprocessing
            • Abstraction-mapping
          • Atc
          • Language
          • Representation
          • Transformation-tools
          • Insertion-sort
          • Pack
        • Bv
        • Imp-language
        • Event-macros
        • Java
        • Bitcoin
        • Ethereum
        • Yul
        • Zcash
        • ACL2-programming-language
        • Prime-fields
        • Json
        • Syntheto
        • File-io-light
        • Cryptography
        • Number-theory
        • Lists-light
        • Axe
        • Builtins
        • Solidity
        • Helpers
        • Htclient
        • Typed-lists-light
        • Arithmetic-light
      • X86isa
      • Axe
      • Execloader
    • Math
    • Testing-utilities
  • Validation-information

Transunit-info

Fixtype of validation information for translation units.

This is a product type introduced by fty::defprod.

Fields
table — valid-table

This is the type of the annotations that the validator adds to translation units. The information consists of the final validation table for the translation unit. We wrap it into a product fixtype for easier future extensibility.

Subtopics

Transunit-info-fix
Fixing function for transunit-info structures.
Transunit-info-equiv
Basic equivalence relation for transunit-info structures.
Make-transunit-info
Basic constructor macro for transunit-info structures.
Transunit-info->table
Get the table field from a transunit-info.
Change-transunit-info
Modifying constructor for transunit-info structures.
Transunit-infop
Recognizer for transunit-info structures.