• 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
                • Asm-name-spec
                • Amb-declor/absdeclor
                • Struni-spec
                  • Struni-specp
                  • Struni-spec-equiv
                  • Make-struni-spec
                  • Struni-spec->members
                  • Change-struni-spec
                  • Struni-spec->name?
                  • Struni-spec->attribs
                  • Struni-spec-fix
                  • Struni-spec-count
                • 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

Struni-spec

Fixtype of structure or union specifiers [C17:6.7.2.1] [C17:A.2.2].

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

Fields
attribs — attrib-spec-list
name? — ident-option
members — struct-declon-list

This corresponds to struct-or-union-specifier in the grammar in [C17], but without the initial struct-or-union. The only use of this fixtype is in type-spec, where we have two separate cases for structures and unions.

This fixtype is a little broader than the grammar, because it allows an absent name and no members. But this definition is simpler, and the disallowed case can be ruled out via predicates over the abstract syntax.

This fixtype does not cover structure types with no members, which is a GCC extension; this is covered as a separate case in type-spec.

As a GCC extension, we allow zero or more attribute specifiers. In the concrete syntax, these come just after struct or union; see the ABNF grammar.

Subtopics

Struni-specp
Recognizer for struni-spec structures.
Struni-spec-equiv
Basic equivalence relation for struni-spec structures.
Make-struni-spec
Basic constructor macro for struni-spec structures.
Struni-spec->members
Get the members field from a struni-spec.
Change-struni-spec
Modifying constructor for struni-spec structures.
Struni-spec->name?
Get the name? field from a struni-spec.
Struni-spec->attribs
Get the attribs field from a struni-spec.
Struni-spec-fix
Fixing function for struni-spec structures.
Struni-spec-count
Measure for recurring over struni-spec structures.