• 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
            • Concrete-syntax
            • Disambiguation
            • Validation
            • Gcc-builtins
            • Preprocessing
              • Preprocessor
                • Pproc
                • Preprocessor-states
                • Preprocessor-printer
                • Pread-token/newline
                • Pread-token
                • Pproc-files
                • Preprocessor-lexer
                • Pproc-file
                  • Pproc-group-part
                  • Pproc-*-group-part
                  • Pproc-directive
                  • *pproc-files-max*
                  • String-plexeme-list-alist-to-filepath-filedata-map
                  • String-plexeme-list-alist
                  • Read-input-file-to-preproc
                  • Preprocessor-reader
                  • Preprocessor-messages
                • External-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
    • Preprocessor
    • Pproc

    Pproc-file

    Preprocess a file.

    Signature
    (pproc-file path file preprocessed preprocessing ienv state) 
      → 
    (mv erp new-preprocessed state)
    Arguments
    path — Guard (stringp path).
    file — Guard (stringp file).
    preprocessed — Guard (string-plexeme-list-alistp preprocessed).
    preprocessing — Guard (string-listp preprocessing).
    ienv — Guard (ienvp ienv).
    Returns
    new-preprocessed — Type (string-plexeme-list-alistp new-preprocessed).

    The file is specified by the file string, which must be either a path relative to the path string, or an absolute path with no relation to path.

    If file is found in the list of the files under preprocessing, we stop with an error, because there is a circularity. If file is found in the alist of already preprocessed files, the alist is returned unchanged.

    Otherwise, we read the file from the file system and preprocess it, which may involve the recursive preprocessing of more files. Before preprocessing the file, we add it to the list of files under preprocessing. We create a local preprocessing state stobj for the file, with information from the implementation environment.