• 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
                • Preprocessor-states
                  • Ppstate
                  • Plexeme
                  • Pnumber
                  • Macro-info
                    • Macro-info-fix
                    • Macro-info-case
                    • Macro-info-function
                    • Macro-info-equiv
                    • Macro-infop
                    • Macro-info-object
                    • Macro-info-kind
                  • Macro-add
                  • Init-ppstate
                  • Plexeme-token/newline-p
                  • Newline
                  • Plexeme-option
                  • Macro-info-option
                  • Macro-table
                  • Plexeme+span
                  • Update-ppstate->lexemes-unread
                  • Update-ppstate->lexemes-read
                  • Update-ppstate->lexemes-length
                  • Update-ppstate->chars-unread
                  • Update-ppstate->chars-read
                  • Update-ppstate->version
                  • Update-ppstate->position
                  • Update-ppstate->macros
                  • Update-ppstate->chars-length
                  • Macro-lookup
                  • Update-ppstate->bytes
                  • Update-ppstate->size
                  • Plexeme-token/space-p
                  • Plexeme-tokenp
                  • Ppstate->gcc
                  • Plexeme-list-token/space-p
                  • Ppstate->size
                  • Ppstate->lexemes-unread
                  • Ppstate->lexemes-read
                  • Ppstate->lexemes-length
                  • Ppstate->chars-unread
                  • Ppstate->bytes
                  • Plexeme-list-token/newline-p
                  • Plexeme-list-not-token/newline-p
                  • Ident-macroinfo-alist
                  • Update-ppstate->lexeme
                  • Update-ppstate->char
                  • Ppstate->version
                  • Ppstate->macros
                  • Ppstate->chars-read
                  • Ppstate->chars-length
                  • Plexeme-list-tokenp
                  • Plexeme-list-not-tokenp
                  • Macro-table-init
                  • Ppstate->lexeme
                  • Ppstate->char
                  • Ppstate-fix
                  • Plexeme+span-list
                  • Plexeme-list
                  • Irr-pnumber
                  • Irr-plexeme
                  • Irr-macro-table
                  • Ppstate->position
                • Pread-token/newline
                • Pread-token
                • Preprocessor-lexer
                • Pproc-files
                • Preprocessor-printer
                • Pproc-file
                • Filepath-plexeme-list-alist-to-filepath-filedata-map
                • Filepath-plexeme-list-alist
                • 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-states

Macro-info

Fixtype of information about a macro.

This is a tagged union type, introduced by fty::deftagsum.

Member Tags → Types
:object → macro-info-object
:function → macro-info-function

This does not include the name, which we represent separately: see macro-table.

Aside from the name, an object-like macro [C17:6.10.3/9] consists of its replacement list, which is a sequence of zero or more preprocessing tokens. To facilitate comparisons with multiple definitions of the same macro [C17:6.10.3/1] [C17:6.10.3/2], we also keep track of whitespace separating tokens, in the form of a single space between two tokens. The invariant plexeme-list-token/space-p captures the fact that we only have tokens and single spaces, but does not capture the fact that the single spaces only occur between two tokens; however, that is also an invariant. The list of lexemes does not include the (mandatory [C17:6.10.3/3]) whitespace between the name and the replacement list, as well as the whitespace after the replacement list, including the closing newline [C17:6.10.3/7].

For a function-like macro [C17:6.10.3/10], besides the replacement list, which we model as for object-like macros (see above), we have zero or more parameters, which are identifiers, and an optional ellipsis parameter, whose presence or absence we model as a boolean. The list of lexemes does not include any whitespace between the closing parenthesis of the parameters and the replacement list, as well as the whitespace after the replacement list, including the closing newline [C17:6.10.3/7].

Subtopics

Macro-info-fix
Fixing function for macro-info structures.
Macro-info-case
Case macro for the different kinds of macro-info structures.
Macro-info-function
Macro-info-equiv
Basic equivalence relation for macro-info structures.
Macro-infop
Recognizer for macro-info structures.
Macro-info-object
Macro-info-kind
Get the kind (tag) of a macro-info structure.