• 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
              • Comp-db-entry
                • Comp-db-entry-fix
                • Comp-db-entry-equiv
                • Make-comp-db-entry
                • Comp-db-entry->arguments
                • Comp-db-entry->output
                • Comp-db-entry->directory
                • Change-comp-db-entry
                • Comp-db-entry->exec
                • Comp-db-entryp
              • Comp-db-arg
              • Json-to-comp-db-entry
              • Json-to-comp-db-entry-list
              • To-preprocess-db
              • To-preprocess-map
              • Comp-db-arguments-absolute-dirs
              • Comp-db-keep-only-preprocessor-args
              • Json-to-comp-db
              • Json-to-comp-db-arguments
              • Comp-db-relativize-keys
              • Json-to-comp-db-get-exec-and-arguments
              • Relativize-path
              • Preprocess-map-from-comp-file
              • Json-to-comp-db-exec-and-arguments
              • Comp-db-arguments-keep-only-preprocessor-args
              • Comp-db-arguments-escape-for-shell
              • Parse-comp-db
              • Json-to-comp-db-get-directory
              • Json-to-comp-db-get-output
              • Json-to-comp-db-get-file
              • Comp-db-drop-shared
              • Comp-db-drop-non-c
              • Comp-db-arg-list-to-string-list
              • Comp-db-absolute-dirs
              • Comp-db-escape-for-shell
              • Json-to-comp-db-try-parse-short-option
              • Preprocess-db-to-map
              • Comp-db-arg-to-string
              • Comp-db
              • Json-to-comp-db-try-parse-equal-arg
              • Defpreprocess-map-fn
              • String-escape-for-shell
              • Comp-db-arg-list
              • Irr-comp-db-arg
              • Show-warnings
              • *cc-options-space-sep*
              • *cc-options-equal-sep*
              • *cc-options-dir*
            • Printer
            • Output-files
            • Abstract-syntax-operations
            • Implementation-environments
            • Abstract-syntax
            • 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
  • Compilation-database

Comp-db-entry

A fixtype for entries parsed from a compilation-database.

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

Fields
exec — stringp
directory — stringp
output — ACL2::string-option
arguments — comp-db-arg-list

The exec field is the executable which performs compilation. The directory is the working directory in which to compile. The optional output field represents the created file (typically a .o file. When present, it is the value associated with the -o flag for C compilations. Lastly, arguments is a list of arguments provided to the compiler.

Subtopics

Comp-db-entry-fix
Fixing function for comp-db-entry structures.
Comp-db-entry-equiv
Basic equivalence relation for comp-db-entry structures.
Make-comp-db-entry
Basic constructor macro for comp-db-entry structures.
Comp-db-entry->arguments
Get the arguments field from a comp-db-entry.
Comp-db-entry->output
Get the output field from a comp-db-entry.
Comp-db-entry->directory
Get the directory field from a comp-db-entry.
Change-comp-db-entry
Modifying constructor for comp-db-entry structures.
Comp-db-entry->exec
Get the exec field from a comp-db-entry.
Comp-db-entryp
Recognizer for comp-db-entry structures.