• 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-cast/logand-to-logand
                • Dimb-cast/and-to-cast
                • Dimb-extdecl-list
                • Dimb-cast/mul-to-cast
                • Dimb-cast/logand-to-cast
                • Dimb-extdecl
                • 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-decl/stmt
                  • Dimb-table
                  • Dimb-pop-scope
                  • Dimb-initdeclor
                  • Dimb-stmt
                  • Dimb-push-scope
                  • Dimb-comp-stmt
                  • Dimb-declor-option
                  • Dimb-enum-spec
                  • Dimb-decl
                  • Dimb-struct-declor
                  • Dimb-scope
                  • Dimb-initdeclor-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-decl-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-param-declor

    Disambiguate a parameter declarator.

    Signature
    (dimb-param-declor paramdeclor table) 
      → 
    (mv erp new-paramdeclor new-table)
    Arguments
    paramdeclor — Guard (param-declorp paramdeclor).
    table — Guard (dimb-tablep table).
    Returns
    erp — Type (maybe-msgp erp).
    new-paramdeclor — Type (param-declorp new-paramdeclor).
    new-table — Type (dimb-tablep new-table).

    A declarator is recursively disambiguated, and the identifier is added to the disambiguation table, as denoting an object or function.

    An abstract declarator is recursively disambiguated, but since it does not introduce an identifier, the disambiguation table is left unchanged.

    An absent parameter declarator is left unchanged, and so is the disambiguation table.

    An ambiguous declarator or abstract declarator is disambiguated to a declarator or abstractor declarator, thus re-classifying the parameter declarator. If the disambiguation is in favor of a declarator, the identifier is also added to the disambiguation table.

    Note that we call dimb-declor with nil as the fundefp flag, because the declarator passed to that function is for a parameter, not for a defined function.