• 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
                • Ident
                • Attrib
                • Amb-declon/stmt
                • Dirabsdeclor
                • Type-qual
                • Fundef
                • Decl-spec
                • Struct-declon
                • Asm-name-spec
                • Amb-declor/absdeclor
                • Struni-spec
                • Param-declor
                • Declor
                • Stor-spec
                • Transunit-ensemble
                • Init-declor
                • Absdeclor
                • Tyname
                • Transunit
                  • Transunitp
                  • Transunit-fix
                  • Transunit-equiv
                  • Make-transunit
                  • Transunit->declons
                  • Change-transunit
                  • Transunit->info
                  • Transunit->comment
                • Keyword-uscores
                • Label
                • Align-spec
                • Expr-option
                • Attrib-name
                • Spec/qual
                • Lsuffix
                • Hex-frac-const
                • Desiniter
                • Param-declon
                • Iconst
                • Dirabsdeclor-option
                • Dec-frac-const
                • Dec-core-fconst
                • Comp-stmt
                • Ext-declon
                • Const-expr-option
                • Amb?-declor/absdeclor
                • Isuffix
                • Hex-core-fconst
                • Attrib-spec
                • Struct-declor
                • Escape
                • Declon
                • Amb?-expr/tyname
                • Initer
                • Ident-option
                • Enum-spec
                • Block-item
                • Bexpo
                • Absdeclor-option
                • Statassert
                • Member-designor
                • Initer-option
                • Declor-option
                • Const
                • Hex-quad
                • Eprefix
                • Const-expr
                • Oct-escape
                • Inc/dec-op
                • Fun-spec
                • Dexpo
                • Cprefix-option
                • Asm-name-spec-option
                • Amb?-declon/stmt
                • S-char
                • Isuffix-option
                • Genassoc
                • Fsuffix-option
                • Fconst
                • Eprefix-option
                • Dexpo-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
                • Asm-qual
                • Typequal/attribspec
                • Stringlit
                • Dexprefix
                • Bexprefix
                • Header-name
                • Cconst
                • Expr/tyname
                • Declor/absdeclor
                • Declon/stmt
                • 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
                • Declon-list
                • C-char-list
                • Typequal/attribspec-list-list
                • Struct-declor-list
                • Struct-declon-list
                • Init-declor-list
                • Genassoc-list
                • Ext-declon-list
                • Block-item-list
                • Ident-list
                • Enumer-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

Transunit

Fixtype of translation units [C17:6.9] [C17:A.2.4].

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

Fields
comment — nat-list
declons — ext-declon-list
info — ACL2::any-p

This corresponds to translation-unit in the grammar in [C17].

A translation unit consists of a list of external declarations, optionally preceded by a line comment, which we represent as its content, namely a list of character codes; the comment is absent if the list is empty. This is useful when generating code: the comment can convey information about the generation. We may eventually generalize this to allow both line and block comments at the top level, intermixed with external declarations, also extending our parser to recognize and preserve those comments (now the tokenizer skips over all comments.

We also add a slot with additional information, e.g. from validation.

Subtopics

Transunitp
Recognizer for transunit structures.
Transunit-fix
Fixing function for transunit structures.
Transunit-equiv
Basic equivalence relation for transunit structures.
Make-transunit
Basic constructor macro for transunit structures.
Transunit->declons
Get the declons field from a transunit.
Change-transunit
Modifying constructor for transunit structures.
Transunit->info
Get the info field from a transunit.
Transunit->comment
Get the comment field from a transunit.