• 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
              • Dimb-exprs/decls/stmts
              • Dimb-make/adjust-expr-binary
              • Dimb-transunit
              • Dimb-params-to-names
              • Dimb-cast/call-to-call
              • Dimb-make/adjust-expr-cast
              • Dimb-fundef
              • Dimb-make/adjust-expr-unary
              • Dimb-expr
              • Dimb-dirdeclor
              • Dimb-amb-declor/absdeclor
              • Dimb-cast/call-to-cast
              • Dimb-cast/addsub-to-cast
              • Dimb-cast/addsub-to-addsub
              • Dimb-transunit-ensemble
              • Dimb-add-ident
              • Dimb-kind
              • Dimb-declor
              • Dimb-amb-expr/tyname
              • Dimb-cast/mul-to-cast
              • Dimb-cast/and-to-cast
              • Dimb-cast/mul-to-mul
              • Dimb-cast/and-to-and
              • Dimb-kind-option
              • Dimb-type-spec
              • Dimb-extdecl-list
              • Dimb-extdecl
              • Dimb-lookup-ident
              • Dimb-param-declor
              • Dimb-decl-spec
              • Dimb-add-idents-objfun
              • Dimb-param-declon
              • Dimb-add-ident-objfun
              • Dimb-table
              • Dimb-amb-decl/stmt
              • Dimb-pop-scope
              • Dimb-push-scope
              • Dimb-initdeclor
                • Dimb-declor-option
                • Dimb-enumspec
                • Dimb-decl
                • Dimb-stmt
                • Dimb-scope
                • Dimb-structdeclor
                • Dimb-initdeclor-list
                • Dimb-decl-spec-list
                • Dimb-absdeclor
                • Dimb-init-table
                • Dimb-dirabsdeclor
                • Dimb-align-spec
                • Dimb-strunispec
                • Irr-dimb-table
                • Irr-dimb-kind
                • Dimb-spec/qual-list
                • Dimb-spec/qual
                • Dimb-param-declon-list
                • Dimb-label
                • Dimb-enumer-list
                • Dimb-enumer
                • Dimb-dirabsdeclor-option
                • Dimb-block-item
                • Dimb-structdeclor-list
                • Dimb-structdecl-list
                • Dimb-statassert
                • Dimb-desiniter-list
                • Dimb-desiniter
                • Dimb-decl-list
                • Dimb-const-expr-option
                • Dimb-absdeclor-option
                • Dimb-structdecl
                • Dimb-member-designor
                • Dimb-initer-option
                • Dimb-initer
                • Dimb-genassoc-list
                • Dimb-genassoc
                • Dimb-expr-option
                • Dimb-expr-list
                • Dimb-designor-list
                • Dimb-designor
                • Dimb-const-expr
                • Dimb-block-item-list
                • Dimb-tyname
              • Abstract-syntax
              • Parser
              • Validator
              • Printer
              • Formalized-subset
              • Mapping-to-language-definition
              • Input-files
              • Defpred
              • Output-files
              • Abstract-syntax-operations
              • Validation-information
              • 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
    • Disambiguator
    • Dimb-exprs/decls/stmts

    Dimb-initdeclor

    Disambiguate an initializer declarator.

    Signature
    (dimb-initdeclor ideclor kind table) 
      → 
    (mv erp new-ideclor new-table)
    Arguments
    ideclor — Guard (initdeclorp ideclor).
    kind — Guard (dimb-kindp kind).
    table — Guard (dimb-tablep table).
    Returns
    new-ideclor — Type (initdeclorp new-ideclor).
    new-table — Type (dimb-tablep new-table).

    An initializer declarator is part of a declaration. At the end of the initializer declarator, the declared identifier is added to the disambiguation table, with the appropriate kind, which comes from the preceding declaration specifiers, and is passed to this function.

    We pass nil as the fundefp flag to dimb-declor, because an initializer declarator is not the declarator of a defined function.