• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Community
    • Proof-automation
    • ACL2
    • Macro-libraries
    • 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-params-to-names
              • Dimb-transunit
              • Dimb-cast/call-to-call
              • Dimb-dirdeclor
              • Dimb-make/adjust-expr-cast
              • Dimb-fundef
              • Dimb-make/adjust-expr-unary
              • Dimb-expr
              • Dimb-amb-declor/absdeclor
              • Dimb-cast/call-to-cast
              • Dimb-declor
                • Dimb-cast/addsub-to-cast
                • Dimb-cast/addsub-to-addsub
                • Dimb-transunit-ensemble
                • Dimb-add-ident
                • Dimb-kind
                • 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-param-declon
                • Dimb-add-idents-objfun
                • 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-struni-spec
                • 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
              • Ascii-identifiers
              • Unambiguity
              • Preprocessing
              • Abstraction-mapping
              • Standard
              • Purity
            • 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 fundef-params-p table) 
      → 
    (mv erp new-declor new-fundef-params-p ident table)
    Arguments
    declor — Guard (declorp declor).
    fundef-params-p — Guard (booleanp fundef-params-p).
    table — Guard (dimb-tablep table).
    Returns
    new-declor — Type (declorp new-declor).
    new-fundef-params-p — Type (booleanp new-fundef-params-p).
    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 fundef-params-p flag is t when this function is called to disambiguate the declarator of a function definition, and only when the parameters of the function have not been disambiguated yet. Its new value new-fundef-params-p, returned as result, stays t if the parameters of the function have still not been disambiguated yet, because they are not found in this declarator; otherwise, its new value is nil. If the input fundef-params-p is nil, then new-fundef-params-p is nil as well. The exact handling of this flag, and the exact treatment of the parameters of function declarations, are explained in dimb-dirdeclor.

    We also pass the fundef-params-p flag to dimb-dirdeclor, and relay the new-fundef-params-p output. The reason is that, after peeling off the pointers, which refine the return result of the function, the direct declarator is still expected to be for a function, and we have not disambiguated the parameters yet.