• 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-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
  • Syntax-for-tools

Compilation-database

Utilities for reading and modifying JSON compilation databases.

The clang ecosystem uses the JSON compilation database format to represent compilation commands. Compilation database files are a convenient way to read the necessary compiler flags for all the source files of a large, complicated project automatically.

Various tools support the generation of compilation database files. On Linux, the Bear tool can be used to generate compilation databases from traditional Makefile-based projects by intercepting and recording compiler calls.

Currently, the primary use-case for compilation database files is to gather all the necessary flags to pass to the C preprocessor.

Subtopics

Comp-db-entry
A fixtype for entries parsed from a compilation-database.
Comp-db-arg
A fixtype for a compiler argument parsed from a compilation-database.
Json-to-comp-db-entry
Json-to-comp-db-entry-list
To-preprocess-db
Transform a compilation-database to prepare for use in preprocessing.
To-preprocess-map
Comp-db-arguments-absolute-dirs
Comp-db-keep-only-preprocessor-args
Filter out compilation-database arguments which are disruptive or irrelevant to preprocessing.
Json-to-comp-db
Json-to-comp-db-arguments
Parse an argument list into structured, name/value 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
Parse a compilation-database from a file.
Json-to-comp-db-get-directory
Json-to-comp-db-get-output
Json-to-comp-db-get-file
Comp-db-drop-shared
Drop compilation-database entries which produce shared or position-independent code.
Comp-db-drop-non-c
Drop compilation-database entries which do not apply to .c file or which don't include a -c flag.
Comp-db-arg-list-to-string-list
Turn a comp-db-arg-list into a string list.
Comp-db-absolute-dirs
Make relative directories absolute in directory-valued arguments of a compilation-database.
Comp-db-escape-for-shell
Escape strings in arguments of a compilation-database for use in the shell.
Json-to-comp-db-try-parse-short-option
Try to parse a short option.
Preprocess-db-to-map
Comp-db-arg-to-string
Turn a comp-db-arg into a string.
Comp-db
A fixtype for parsed compilation-databases.
Json-to-comp-db-try-parse-equal-arg
Try to parse an argument with an = separator.
Defpreprocess-map-fn
String-escape-for-shell
Escape characters interpreted specially by the shell.
Comp-db-arg-list
A fixtype for lists of compiler arguments parsed from a compilation-database.
Irr-comp-db-arg
An irrelevant comp-db-arg.
Show-warnings
*cc-options-space-sep*
C flags whose value follows after a whitespace separator.
*cc-options-equal-sep*
C flags whose value follows after an = character.
*cc-options-dir*
C flags whose value represents a directory.