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

    Disambiguate a direct declarator.

    Signature
    (dimb-dirdeclor dirdeclor fundefp table) 
      → 
    (mv erp new-dirdeclor ident new-table)
    Arguments
    dirdeclor — Guard (dirdeclorp dirdeclor).
    fundefp — Guard (booleanp fundefp).
    table — Guard (dimb-tablep table).
    Returns
    erp — Type (maybe-msgp erp).
    new-dirdeclor — Type (dirdeclorp new-dirdeclor).
    ident — Type (identp ident).
    new-table — Type (dimb-tablep new-table).

    As explained in dimb-declor, a (direct) declarator adds an identifier to the scope. So here we return the identifer, recursively extracted from the direct declarator. The actual addition to the disambiguation table is performed outside this function.

    The meaning of the fundefp flag passed as input is the same as in dimb-declor: see that function's documentation.

    We recursively disambiguate the inner declarator and direct declarator, from which we obtain the identifier. We also recursively disambiguate any expressions in array declarators.

    For function declarators, the parser only produces :function-params, never :function-names. However, here we also process :function-names, so that the disambiguator is idempotent. We push a new scope, for uniformity with the treatment described in the next paragraph.

    For a :function-params, first we attempt to turn it into a :function-names, if applicable. We pass fundefp to dimb-params-to-names, which indicates whether the parameters in question are for a function definition or not. If this flag is t, and this is the innermost :function-params (see explanation later), we push a new scope for the function parameters and body, but it will be the declarations between the parameter names and the body that will populate the newly pushed scope. If this flag is nil, we do not push a new scope, because it just means that the list of parameters is empty, but they are not the parameters of a function definition; it is just a function prototype with no parameters.

    If we cannot turn the :function-params into a :function-names, we push a new scope for the parameters, and we disambiguate the parameters (which adds them to the new scope). Then, if fundefp is t and this is the innermost :function-params (see explanation later), we leave the previously pushed scope in the disambiguation table, so it is available for the body of the function; otherwise, we pop that scope.

    The reason for the dirdeclor-has-params-p can be seen from the example function definition

    void (*f(float x, double y))(int z) {
      ...
    }

    The parameters of the function are x and y, not z. But when we disambiguate the declarator, we first encounter the :function-params with z. But the inner declarator satisfies dirdeclor-has-params-p, which means that the :function-params with z does not form the parameters of the function being defined; thus, we pop the function prototype scope [C17:6.2.1/4] from the table in this case. When instead we reach the inner :function-params, i.e. the one with x and y, we leave the scope on the table, because that forms the parameters of the function definition.