• 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
          • Atc
          • Language
            • Abstract-syntax
              • Tyspecseq
              • Expr
              • Binop
              • Fileset
                • Fileset-fix
                • Filesetp
                • Fileset-equiv
                • Make-fileset
                • Fileset->path-wo-ext
                • Change-fileset
                • Fileset->dot-h
                • Fileset->dot-c
              • Obj-declor
              • Ident
              • Iconst
              • Obj-adeclor
              • Const
              • Fundef
              • Unop
              • File
              • Tag-declon
              • Fun-declor
              • Obj-declon
              • Iconst-length
              • Abstract-syntax-operations
              • Label
              • Struct-declon
              • Initer
              • Ext-declon
              • Fun-adeclor
              • Expr-option
              • Iconst-base
              • Initer-option
              • Iconst-option
              • Tyspecseq-option
              • Stmt-option
              • Scspecseq
              • Param-declon
              • Obj-declon-option
              • File-option
              • Tyname
              • Transunit
              • Fun-declon
              • Transunit-result
              • Param-declon-list
              • Struct-declon-list
              • Expr-list
              • Tyspecseq-list
              • Ident-set
              • Ident-list
              • Ext-declon-list
              • Unop-list
              • Tyname-list
              • Fundef-list
              • Fun-declon-list
              • Binop-list
              • Stmt-fixtypes
              • Expr-fixtypes
            • Integer-ranges
            • Implementation-environments
            • Dynamic-semantics
            • Static-semantics
            • Grammar
            • Integer-formats
            • Types
            • Portable-ascii-identifiers
            • Values
            • Integer-operations
            • Computation-states
            • Object-designators
            • Operations
            • Errors
            • Tag-environments
            • Function-environments
            • Character-sets
            • Flexible-array-member-removal
            • Arithmetic-operations
            • Pointer-operations
            • Bytes
            • Keywords
            • Real-operations
            • Array-operations
            • Scalar-operations
            • Structure-operations
          • 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

Fileset

Fixtype of file sets.

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

Fields
path-wo-ext — stringp
dot-h — file-option
dot-c — file

A file set is a collection of related files. This is not an explicit notion in [C17], but it is a useful one in a language formalization: a program, or a portion of a program, is contained in a set of related files. This notion is not quite the same as that of C program, which, according to [C17], is a complete executable application: a library would not qualify as a program in this sense.

For now, a file set consists of one or two files (see file), namely an optional header and a source file, which have the same name except for the extension. (The preceding sentence uses the terminology in [C17:5.1.1/1], which appears to call `headers' the .h files and `source files' the .c files.) The idea is that for now we model (portions of) programs that consist of a single source file, optionally with its own header that is #included in the source file. We do not explicitly model the #include directive: it is implicit. The path-wo-ext component of this fixtype is the common path of both files without the extension. The dot-h and dot-c components of this fixtype are (the contents of) the .h and .c files, where the first one is optional.

In the future, we may extend this notion of file set to be something like a finite map from file system paths to (contents of) files.

The notion of file set defined here is related to the one defined in c$::fileset, where it is actually part of the concrete (not abstract) syntax for tools. We plan to make the overall nomenclature more consistent at some point.

Subtopics

Fileset-fix
Fixing function for fileset structures.
Filesetp
Recognizer for fileset structures.
Fileset-equiv
Basic equivalence relation for fileset structures.
Make-fileset
Basic constructor macro for fileset structures.
Fileset->path-wo-ext
Get the path-wo-ext field from a fileset.
Change-fileset
Modifying constructor for fileset structures.
Fileset->dot-h
Get the dot-h field from a fileset.
Fileset->dot-c
Get the dot-c field from a fileset.