• 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
              • Disambiguator
                • Dimb-exprs/decls/stmts
                  • Dimb-dirdeclor
                  • Dimb-expr
                  • Dimb-amb-declor/absdeclor
                  • Dimb-amb-expr/tyname
                  • Dimb-declor
                    • Dimb-type-spec
                    • Dimb-param-declor
                    • Dimb-decl-spec
                    • Dimb-param-declon
                    • Dimb-amb-declon/stmt
                    • Dimb-init-declor
                    • Dimb-stmt
                    • Dimb-comp-stmt
                    • Dimb-declor-option
                    • Dimb-enum-spec
                    • Dimb-declon
                    • Dimb-struct-declor
                    • Dimb-init-declor-list
                    • Dimb-decl-spec-list
                    • Dimb-absdeclor
                    • Dimb-dirabsdeclor
                    • Dimb-align-spec
                    • Dimb-struni-spec
                    • Dimb-spec/qual-list
                    • Dimb-spec/qual
                    • Dimb-param-declon-list
                    • Dimb-enumer-list
                    • Dimb-enumer
                    • Dimb-dirabsdeclor-option
                    • Dimb-block-item
                    • Dimb-struct-declor-list
                    • Dimb-struct-declon-list
                    • Dimb-struct-declon
                    • Dimb-statassert
                    • Dimb-label
                    • Dimb-desiniter-list
                    • Dimb-desiniter
                    • Dimb-declon-list
                    • Dimb-const-expr-option
                    • Dimb-absdeclor-option
                    • Dimb-member-designor
                    • Dimb-initer-option
                    • 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
                    • Dimb-initer
                  • Dimb-make/adjust-expr-cast
                  • Dimb-make/adjust-expr-binary
                  • Dimb-params-to-names
                  • Dimb-fundef
                  • Dimb-cast/call-to-call
                  • Dimb-transunit
                  • Dimb-dirdeclor
                  • Dimb-transunit-ensemble
                  • Dimb-make/adjust-expr-unary
                  • Dimb-expr
                  • Dimb-amb-declor/absdeclor
                  • Dimb-cast/call-to-cast
                  • Dimb-cast/addsub-to-cast
                  • Dimb-cast/addsub-to-addsub
                  • Dimb-add-ident
                  • Dimb-kind
                  • Dimb-amb-expr/tyname
                  • Dimb-ext-declon-list
                  • Dimb-ext-declon
                  • Dimb-cast/logand-to-logand
                  • Dimb-cast/and-to-cast
                  • Dimb-cast/mul-to-cast
                  • Dimb-cast/logand-to-cast
                  • Dimb-cast/mul-to-mul
                  • Dimb-cast/and-to-and
                  • Dimb-declor
                    • Dimb-kind-option
                    • Dimb-type-spec
                    • Dimb-add-ident-objfun-file-scope
                    • Dimb-make/adjust-expr-label-addr
                    • Dimb-param-declor
                    • Dimb-lookup-ident
                    • Dimb-decl-spec
                    • Dimb-add-idents-objfun
                    • Dimb-add-ident-objfun
                    • Dimb-param-declon
                    • Dimb-amb-declon/stmt
                    • Dimb-table
                    • Dimb-pop-scope
                    • Dimb-init-declor
                    • Dimb-stmt
                    • Dimb-push-scope
                    • Dimb-comp-stmt
                    • Dimb-declor-option
                    • Dimb-enum-spec
                    • Dimb-declon
                    • Dimb-struct-declor
                    • Dimb-scope
                    • Dimb-init-declor-list
                    • Dimb-decl-spec-list
                    • Dimb-absdeclor
                    • Dimb-dirabsdeclor
                    • Dimb-align-spec
                    • Dimb-struni-spec
                    • Dimb-init-table
                    • Dimb-spec/qual-list
                    • Dimb-spec/qual
                    • Irr-dimb-table
                    • Irr-dimb-kind
                    • Dimb-param-declon-list
                    • Dimb-enumer-list
                    • Dimb-enumer
                    • Dimb-dirabsdeclor-option
                    • Dimb-block-item
                    • Dimb-struct-declor-list
                    • Dimb-struct-declon-list
                    • Dimb-struct-declon
                    • Dimb-statassert
                    • Dimb-label
                    • Dimb-desiniter-list
                    • Dimb-desiniter
                    • Dimb-declon-list
                    • Dimb-const-expr-option
                    • Dimb-absdeclor-option
                    • Dimb-member-designor
                    • Dimb-initer-option
                    • 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
                    • Dimb-initer
                  • Unambiguity
                • Validation
                • 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
      • 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
      erp — Type (maybe-msgp erp).
      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 is t when this function is called to disambiguate the declarator of a function definition.

      We also pass the fundefp flag to dimb-dirdeclor. 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.