• 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
              • Abstract-syntax-trees
                • Expr
                • Type-spec
                • Exprs/decls/stmts
                • Binop
                • Stmt
                • Unop
                • Amb-expr/tyname
                • Dirdeclor
                • Asm-stmt
                • Dec/oct/hex-const
                • Simple-escape
                • Fsuffix
                • Attrib
                • Ident
                • Amb-decl/stmt
                • Dirabsdeclor
                • Type-qual
                • Decl-spec
                • Fundef
                • Struct-declon
                  • Struct-declon-case
                  • Struct-declonp
                  • Struct-declon-equiv
                  • Struct-declon-member
                  • Struct-declon-statassert
                  • Struct-declon-empty
                  • Struct-declon-kind
                  • Struct-declon-fix
                  • Struct-declon-count
                • Asm-name-spec
                • Amb-declor/absdeclor
                • Struni-spec
                • Param-declor
                • Declor
                • Stor-spec
                • Transunit-ensemble
                • Initdeclor
                • Absdeclor
                • Tyname
                • Keyword-uscores
                • Label
                • Align-spec
                • Expr-option
                • Spec/qual
                • Lsuffix
                • Hex-frac-const
                • Desiniter
                • Param-declon
                • Iconst
                • Dirabsdeclor-option
                • Dec-frac-const
                • Dec-core-fconst
                • Comp-stmt
                • Extdecl
                • Const-expr-option
                • Amb?-declor/absdeclor
                • Isuffix
                • Hex-core-fconst
                • Attrib-spec
                • Struct-declor
                • Escape
                • Decl
                • Amb?-expr/tyname
                • Initer
                • Ident-option
                • Bin-expo
                • Absdeclor-option
                • Statassert
                • Member-designor
                • Initer-option
                • Enum-spec
                • Declor-option
                • Const
                • Block-item
                • Hex-quad
                • Eprefix
                • Const-expr
                • Oct-escape
                • Inc/dec-op
                • Fun-spec
                • Dec-expo
                • Cprefix-option
                • Asm-name-spec-option
                • Amb?-decl/stmt
                • S-char
                • Isuffix-option
                • Genassoc
                • Fsuffix-option
                • Fconst
                • Eprefix-option
                • Dec-expo-option
                • Cprefix
                • C-char
                • Type-spec-option
                • Sign-option
                • Sign
                • Q-char
                • Iconst-option
                • H-char
                • Fundef-option
                • Asm-output
                • Asm-input
                • Designor
                • Const-option
                • Usuffix
                • Univ-char-name
                • Hprefix
                • Enumer
                • Attrib-name
                • Transunit
                • Asm-qual
                • Typequal/attribspec
                • Stringlit
                • Dec-expo-prefix
                • Bin-expo-prefix
                • Header-name
                • 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
                • Attrib-spec-list
                • S-char-list
                • Q-char-list
                • Param-declon-list
                • H-char-list
                • Decl-list
                • C-char-list
                • Typequal/attribspec-list-list
                • Struct-declor-list
                • Struct-declon-list
                • Initdeclor-list
                • Genassoc-list
                • Extdecl-list
                • Block-item-list
                • Enumer-list
                • Ident-list
                • Filepath-transunit-map
                • Expr-list
                • Asm-qual-list
                • Asm-output-list
                • Asm-input-list
                • Asm-clobber-list
                • Type-spec-list
                • Stor-spec-list
                • Ident-set
                • Ident-option-set
                • Ident-list-list
                • Eprefix-option-list
                • Designor-list
                • Attrib-list
              • Abstract-syntax-irrelevants
              • Type-specifier-lists
              • Ascii-identifiers
              • Abstraction-mapping
              • Standard
              • Storage-specifier-lists
              • Code-ensembles
              • Purity
              • Make-self-code-ensemble
            • Concrete-syntax
            • Disambiguation
            • 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
  • Abstract-syntax-trees
  • Exprs/decls/stmts

Struct-declon

Fixtype of structure declarations [C17:6.7.2.1] [C17:A.2.2].

This is a tagged union type, introduced by fty::deftagsum.

Member Tags → Types
:member → struct-declon-member
:statassert → struct-declon-statassert
:empty → struct-declon-empty

This corresponds to struct-declaration in the grammar of [C17]. Despite its name in the grammar and in this fixtype, this applies to both structures and unions; in fact, it is not a declaration of a structure, but instead it is a declaration of a member of a structure or union. So something like member-declaration would be a better name for this grammar nonterminal, but our fixtype name reflects the current grammar.

As a GCC extension, we include the possibility that a member declaration starts with the __extension__ GCC keyword. We model that as a boolean that says whether that keyword is present or absent.

As a GCC extension, we include a possibly empty list of attribute specifiers, which come after the declarator (cf. the grammar).

As explained in our ABNF grammar, we also include an empty external declaration, which syntactically consists of a semicolon.

Subtopics

Struct-declon-case
Case macro for the different kinds of struct-declon structures.
Struct-declonp
Recognizer for struct-declon structures.
Struct-declon-equiv
Basic equivalence relation for struct-declon structures.
Struct-declon-member
Struct-declon-statassert
Struct-declon-empty
Struct-declon-kind
Get the kind (tag) of a struct-declon structure.
Struct-declon-fix
Fixing function for struct-declon structures.
Struct-declon-count
Measure for recurring over struct-declon structures.