• 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
            • Parser
            • Validator
            • Printer
              • Print-exprs/decls/stmts
              • Print-expr
              • Pristate
              • Print-fileset
              • Print-dec/oct/hex-const
              • Priopt
              • Print-fundef
              • Print-s-char
              • Print-c-char
              • Print-typequal/attribspec-list-list
              • Print-ident
              • Print-ident-list
              • Print-hex-core-fconst
              • Print-dec-core-fconst
              • Print-oct-digit-achar
              • Print-hex-frac-const
              • Print-hex-digit-achar
              • Print-dec-frac-const
              • Print-dec-digit-achar
              • Print-strunispec
                • Print-file
                • Print-astring
                • Print-asm-name-spec
                • Print-asm-clobber-list
                • Print-stringlit-list
                • Print-inc/dec-op-list
                • Print-cprefix-option
                • Print-binop
                • Print-univ-char-name
                • Print-type-qual
                • Print-transunit
                • Print-simple-escape
                • Print-s-char-list
                • Print-isuffix-option
                • Print-indent
                • Print-fsuffix-option
                • Print-extdecl-list
                • Print-eprefix-option
                • Print-dec-expo-option
                • Print-char
                • Print-c-char-list
                • Print-attrib-name
                • Print-asm-qual-list
                • Print-stor-spec
                • Print-oct-escape
                • Print-escape
                • Print-dec-expo-prefix
                • Print-cconst
                • Print-bin-expo-prefix
                • Dec-pristate-indent
                • Print-stringlit
                • Print-sign-option
                • Print-isuffix
                • Print-fun-spec
                • Print-fconst
                • Print-extdecl
                • Print-dec-expo
                • Print-block
                • Print-bin-expo
                • Print-asm-qual
                • Print-asm-clobber
                • Print-new-line
                • Print-lsuffix
                • Print-inc/dec-op
                • Print-hex-quad
                • Print-fsuffix
                • Print-eprefix
                • Print-cprefix
                • Print-usuffix
                • Print-unop
                • Print-iconst
                • Print-hprefix
                • Print-const
                • Print-chars
                • Print-sign
                • Print-oct-digit-achars
                • Print-hex-digit-achars
                • Print-dec-digit-achars
                • Print-stmt
                • Print-expr-list
                • Init-pristate
                • Print-structdecl-list
                • Inc-pristate-indent
                • Print-param-declor
                • Print-dirdeclor
                • Default-priopt
                • Print-structdeclor
                • Print-initer
                • Print-decl-inline
                • Print-structdecl
                • Print-genassoc-list
                • Print-enumspec
                • Print-absdeclor
                • Print-typequal/attribspec-list
                • Print-desiniter-list
                • Print-const-expr
                • Print-attrib
                • Print-tyname
                • Print-structdeclor-list
                • Print-spec/qual-list
                • Print-param-declon-list
                • Print-param-declon
                • Print-initdeclor-list
                • Print-designor-list
                • Print-decl-spec-list
                • Print-decl-list
                • Print-attrib-spec-list
                • Print-asm-output-list
                • Print-asm-input-list
                • Print-typequal/attribspec
                • Print-statassert
                • Print-spec/qual
                • Print-member-designor
                • Print-initdeclor
                • Print-enumer-list
                • Print-dirabsdeclor
                • Print-desiniter
                • Print-decl-spec
                • Print-decl
                • Print-block-item-list
                • Print-attrib-spec
                • Print-attrib-list
                • Print-asm-output
                • Print-align-spec
                • Print-type-spec
                • Print-label
                • Print-genassoc
                • Print-enumer
                • Print-designor
                • Print-declor
                • Print-block-item
                • Print-asm-stmt
                • Print-asm-input
              • 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
    • Printer
    • Print-exprs/decls/stmts

    Print-strunispec

    Print a structure or union specifier.

    Signature
    (print-strunispec strunispec pstate) → new-pstate
    Arguments
    strunispec — Guard (strunispecp strunispec).
    pstate — Guard (pristatep pstate).
    Returns
    new-pstate — Type (pristatep new-pstate).

    This is called after printing the struct or union keyword followed by a space. Here we print what comes after that keyword.

    We ensure that this is not empty, i.e. that there is at least the identifier or a non-empty member list.

    For now we print all the members in the same line, but we should print them in different lines and with identation, at least in certain cases. Note that a structure or union specifier is not necessarily a top-level construct: it may occur in the middle of a sequence of declaration specifiers, so it is not so straightforward to always print it on multiple lines, because we may need to consider what surrounds it. Nonetheless, under certain conditions, e.g. when it is a lone top-level construct, we should print it on multiple lines.