• 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
                • Absdeclor
                • Strunispec
                  • Strunispec-equiv
                  • Strunispecp
                  • Make-strunispec
                  • Strunispec->members
                  • Strunispec->name
                  • Change-strunispec
                  • Strunispec-fix
                  • Strunispec-count
                • 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
              • Type-qual
              • Absdeclor
              • Strunispec
                • Strunispec-equiv
                • Strunispecp
                • Make-strunispec
                • Strunispec->members
                • Strunispec->name
                • Change-strunispec
                • Strunispec-fix
                • Strunispec-count
              • 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

Strunispec

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
name — ident-option
members — structdecl-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.

Subtopics

Strunispec-equiv
Basic equivalence relation for strunispec structures.
Strunispecp
Recognizer for strunispec structures.
Make-strunispec
Basic constructor macro for strunispec structures.
Strunispec->members
Get the members field from a strunispec.
Strunispec->name
Get the name field from a strunispec.
Change-strunispec
Modifying constructor for strunispec structures.
Strunispec-fix
Fixing function for strunispec structures.
Strunispec-count
Measure for recurring over strunispec structures.