• 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
                  • Structdecl-case
                  • Structdeclp
                  • Structdecl-member
                  • Structdecl-equiv
                  • Structdecl-statassert
                  • Structdecl-kind
                  • Structdecl-empty
                  • Structdecl-fix
                  • Structdecl-count
                • Amb-declor/absdeclor
                • Param-declor
                • Declor
                • 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
                • Structdecl-case
                • Structdeclp
                • Structdecl-member
                • Structdecl-equiv
                • Structdecl-statassert
                • Structdecl-kind
                • Structdecl-empty
                • Structdecl-fix
                • Structdecl-count
              • Fundef
              • Transunit-ensemble
              • Asm-name-spec
              • Amb-declor/absdeclor
              • Param-declor
              • Declor
              • 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

Structdecl

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 → structdecl-member
:statassert → structdecl-statassert
:empty → structdecl-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

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