• 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
                  • Pproc-file
                  • Pproc-group-part
                  • Pproc-*-group-part
                  • Pproc-directive
                  • 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-directive

      Preprocess a directive.

      Signature
      (pproc-directive path file preprocessed 
                       preprocessing rev-lexemes ppstate state) 
       
        → 
      (mv erp new-rev-lexemes new-ppstate new-preprocessed state)
      Arguments
      path — Guard (stringp path).
      file — Guard (stringp file).
      preprocessed — Guard (string-plexeme-list-alistp preprocessed).
      preprocessing — Guard (string-listp preprocessing).
      rev-lexemes — Guard (plexeme-listp rev-lexemes).
      ppstate — Guard (ppstatep ppstate).
      Returns
      new-rev-lexemes — Type (plexeme-listp new-rev-lexemes).
      new-ppstate — Type (ppstatep new-ppstate), given (ppstatep ppstate).
      new-preprocessed — Type (string-plexeme-list-alistp new-preprocessed).

      With reference to the grammar, a directive is a group part that starts with #; this function is called just after the # has been encountered. A directive may be an if group (which spans multiple lines), a control line (which spans one line), or a non-directive (which spans one line); the latter, despite the name, is considered a directive (see footnote 175 in [C17:6.10.3/11].