• 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
            • Abstract-syntax
              • Expr
              • Exprs/decls/stmts
                • Expr
                • Type-spec
                • Stmt
                • Amb-expr/tyname
                • Dirdeclor
                • Asm-stmt
                • Attrib
                • Amb-decl/stmt
                • Dirabsdeclor
                • Decl-spec
                • Structdecl
                • Amb-declor/absdeclor
                • Param-declor
                • Declor
                  • Declorp
                  • Declor-equiv
                  • Make-declor
                  • Declor->pointers
                  • Declor->direct
                  • Change-declor
                  • Declor-fix
                  • Declor-count
                • Absdeclor
                • Strunispec
                • Align-spec
                • Label
                • Expr-option
                • Spec/qual
                • Desiniter
                • Tyname
                • Dirabsdeclor-option
                • Initdeclor
                • Const-expr-option
                • Attrib-spec
                • Structdeclor
                • Decl
                • Absdeclor-option
                • Statassert
                • Param-declon
                • Member-designor
                • Initer-option
                • Initer
                • Enumspec
                • Declor-option
                • Const-expr
                • Block-item
                • Genassoc
                • Asm-output
                • Asm-input
                • Enumer
                • Designor
                • Typequal/attribspec
                • Typequal/attribspec-list
                • Decl-spec-list
                • Spec/qual-list
                • Desiniter-list
                • Param-declon-list
                • Decl-list
                • Block-item-list
                • Typequal/attribspec-list-list
                • Structdeclor-list
                • Structdecl-list
                • Initdeclor-list
                • Genassoc-list
                • Expr-list
                • Enumer-list
                • Attrib-spec-list
                • Asm-output-list
                • Asm-input-list
                • Designor-list
                • Attrib-list
              • Type-spec
              • Binop
              • Stmt
              • Amb-expr/tyname
              • Dirdeclor
              • Unop
              • Asm-stmt
              • Dec/oct/hex-const
              • Simple-escape
              • Attrib
              • Ident
              • Amb-decl/stmt
              • Dirabsdeclor
              • Decl-spec
              • Structdecl
              • Fundef
              • Transunit-ensemble
              • Asm-name-spec
              • Amb-declor/absdeclor
              • Param-declor
              • Declor
                • Declorp
                • Declor-equiv
                • Make-declor
                • Declor->pointers
                • Declor->direct
                • Change-declor
                • Declor-fix
                • Declor-count
              • Type-qual
              • Absdeclor
              • Strunispec
              • Stor-spec
              • Keyword-uscores
              • Align-spec
              • Label
              • Expr-option
              • Spec/qual
              • Lsuffix
              • Hex-frac-const
              • Desiniter
              • Tyname
              • Iconst
              • Dirabsdeclor-option
              • Dec-frac-const
              • Dec-core-fconst
              • Extdecl
              • Amb?-declor/absdeclor
              • Isuffix
              • Initdeclor
              • Hex-core-fconst
              • Const-expr-option
              • Attrib-spec
              • Structdeclor
              • Escape
              • Decl
              • Amb?-expr/tyname
              • Ident-option
              • Bin-expo
              • Absdeclor-option
              • Statassert
              • Param-declon
              • Member-designor
              • Initer-option
              • Initer
              • Fsuffix
              • Enumspec
              • Declor-option
              • Const
              • Hex-quad
              • Eprefix
              • Const-expr
              • Block-item
              • Oct-escape
              • Inc/dec-op
              • Fun-spec
              • Dec-expo
              • Cprefix-option
              • Asm-name-spec-option
              • Amb?-decl/stmt
              • S-char
              • Isuffix-option
              • Genassoc
              • Fundef-option
              • Fsuffix-option
              • Fconst
              • Eprefix-option
              • Dec-expo-option
              • Cprefix
              • C-char
              • Type-spec-option
              • Sign-option
              • Iconst-option
              • Asm-output
              • Asm-input
              • Const-option
              • Usuffix
              • Univ-char-name
              • Transunit
              • Hprefix
              • Enumer
              • Designor
              • Attrib-name
              • Sign
              • Asm-qual
              • Typequal/attribspec
              • Dec-expo-prefix
              • Bin-expo-prefix
              • Stringlit
              • Cconst
              • Expr/tyname
              • Decl/stmt
              • Declor/absdeclor
              • Asm-clobber
              • Typequal/attribspec-list
              • Decl-spec-list
              • Stringlit-list
              • Spec/qual-list
              • Inc/dec-op-list
              • Desiniter-list
              • S-char-list
              • Param-declon-list
              • Decl-list
              • C-char-list
              • Block-item-list
              • Typequal/attribspec-list-list
              • Structdeclor-list
              • Structdecl-list
              • Initdeclor-list
              • Genassoc-list
              • Filepath-transunit-map
              • Extdecl-list
              • Expr-list
              • Enumer-list
              • Attrib-spec-list
              • Type-spec-list
              • Ident-list
              • Asm-qual-list
              • Asm-output-list
              • Asm-input-list
              • Asm-clobber-list
              • Stor-spec-list
              • Ident-set
              • Ident-option-set
              • Eprefix-option-list
              • Designor-list
              • Attrib-list
            • 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
  • Abstract-syntax
  • Exprs/decls/stmts

Declor

Fixtype of declarators [C17:6.7.6] [C17:A.2.2].

This is a product type introduced by fty::defprod.

Fields
pointers — typequal/attribspec-list-list
direct — dirdeclor

This corresponds to declarator in the grammar in [C17]. The optional pointer that precedes the direct-declarator is a sequence of stars each optionally followed by an optional sequence of type qualifiers and attribute specifiers. We model this as a list of lists of type qualifiers and attribute specifiers: the outer list corresponds to each star, and each inner list corresponds to the type qualifiers and attribute specifiers that immediately follow the star.

Subtopics

Declorp
Recognizer for declor structures.
Declor-equiv
Basic equivalence relation for declor structures.
Make-declor
Basic constructor macro for declor structures.
Declor->pointers
Get the pointers field from a declor.
Declor->direct
Get the direct field from a declor.
Change-declor
Modifying constructor for declor structures.
Declor-fix
Fixing function for declor structures.
Declor-count
Measure for recurring over declor structures.