• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Community
    • 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
        • C
          • Syntax-for-tools
            • Formalized-subset
            • Mapping-to-language-definition
            • Input-files
            • Compilation-database
            • Printer
            • Output-files
            • Abstract-syntax-operations
            • Implementation-environments
            • Abstract-syntax
            • Concrete-syntax
            • Disambiguation
            • Validation
              • Validator
              • Validation-information
                • Abstract-syntax-annop
                • Types
                • Abstract-syntax-anno-additional-theroems
                • Valid-ext-info
                • Valid-table
                • Valid-ord-info
                • Uid
                • Stmts-types
                • Lifetime
                • Initdeclor-info
                  • Initdeclor-info-fix
                  • Initdeclor-info-equiv
                  • Make-initdeclor-info
                  • Initdeclor-info->uid?
                  • Initdeclor-info->typedefp
                  • Change-initdeclor-info
                  • Initdeclor-info->type
                  • Initdeclor-infop
                • Fundef-types
                • Expr-type
                • Valid-defstatus
                • Var-info
                • Valid-ord-info-option
                • Valid-ext-info-option
                • Uid-option
                • Linkage-option
                • Linkage
                • Lifetime-option
                • Valid-table-option
                • Iconst-info
                • Param-declor-nonabstract-info
                • Fundef-info
                • Expr-null-pointer-constp
                • Valid-scope
                • Const-expr-null-pointer-constp
                • Expr-string-info
                • Expr-funcall-info
                • Expr-arrsub-info
                • Tyname-info
                • Transunit-info
                • Expr-unary-info
                • Expr-const-info
                • Expr-binary-info
                • Stmt-types
                • Block-item-list-types
                • Initer-type
                • Valid-ord-scope
                • Uid-increment
                • Uid-equal
                • Coerce-var-info
                • Valid-externals
                • Irr-var-info
                • Valid-scope-list
                • Irr-valid-table
                • Irr-lifetime
                • Irr-uid
                • Irr-linkage
                • Block-item-types
                • Comp-stmt-types
            • Gcc-builtins
            • Preprocessing
            • Parsing
          • Atc
          • Transformation-tools
          • Language
          • Representation
          • Insertion-sort
          • Pack
        • Soft
        • Bv
        • Imp-language
        • Ethereum
        • Event-macros
        • Java
        • Riscv
        • Bitcoin
        • Zcash
        • Yul
        • ACL2-programming-language
        • Prime-fields
        • Json
        • Syntheto
        • File-io-light
        • Cryptography
        • Number-theory
        • Axe
        • Lists-light
        • Builtins
        • Solidity
        • Helpers
        • Htclient
        • Typed-lists-light
        • Arithmetic-light
      • X86isa
      • Axe
      • Execloader
    • Math
    • Testing-utilities
  • Validation-information

Initdeclor-info

Fixtype of validation information for initializer declarators.

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

Fields
type — type
typedefp — booleanp
uid? — uid-option

This is the type of the annotations that the validator adds to initializer declarators, i.e. the initdeclor fixtype.

The information for an initializer declarator consists of the type of (or denoted by) the declared identifier, a flag saying whether the identifier is a typdef or not (if the flag is t the type is the one denoted by the identifier), and an optional unique identifier. Currently, we only assign unique identifiers to ordinary identifiers representing an object or function. Therefore, only initializer declarators corresponding to those such identifiers are annotated with unique identifiers. Initializer declarators which correspond to typedef declarations are not annotated with a unique identifier.

Subtopics

Initdeclor-info-fix
Fixing function for initdeclor-info structures.
Initdeclor-info-equiv
Basic equivalence relation for initdeclor-info structures.
Make-initdeclor-info
Basic constructor macro for initdeclor-info structures.
Initdeclor-info->uid?
Get the uid? field from a initdeclor-info.
Initdeclor-info->typedefp
Get the typedefp field from a initdeclor-info.
Change-initdeclor-info
Modifying constructor for initdeclor-info structures.
Initdeclor-info->type
Get the type field from a initdeclor-info.
Initdeclor-infop
Recognizer for initdeclor-info structures.