• 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-declor

    Disambiguate a declarator.

    Signature
    (dimb-declor declor fundefp table) 
      → 
    (mv erp new-declor ident table)
    Arguments
    declor — Guard (declorp declor).
    fundefp — Guard (booleanp fundefp).
    table — Guard (dimb-tablep table).
    Returns
    new-declor — Type (declorp new-declor).
    ident — Type (identp ident).
    table — Type (dimb-tablep table).

    A declarator adds an identifier to the scope. This function returns the identifier. Its addition to the disambiguation table is performed outside of this function, after processing the top-level declarator in the construct of interest.

    The pointer part of a declarator does not contribute to the table and does not need to be disambiguated. So we recursively disambiguate the direct declarator, which also gives us the identifier, and then we re-add the pointer part.

    The fundefp flag passed to this function says whether we are disambiguating the declarator of a function definition or not. It is used to determine whether, when disambiguating the parameters of a function declarator, the new scope pushed for the function prototype should be popped at the end of the function declarator or not. If the declarator is not part of a function definition, then that scope must be popped; but if instead the declarator is part of a function definition, that scope is the block scope of the definition, and must not be popped. Here by `part of a function definition' of course we mean the one that introduces the name of the function being defined.