Skip to content
New issue

Have a question about this project? # for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “#”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? # to your account

Add Compilation Database support #448

Merged
merged 34 commits into from
Nov 23, 2021
Merged

Add Compilation Database support #448

merged 34 commits into from
Nov 23, 2021

Conversation

sim642
Copy link
Member

@sim642 sim642 commented Nov 12, 2021

Closes #406.

So far I've just tested it with this tiny example CMake project I set up: https://github.com/sim642/goblint-action-test/tree/compilation-database/cmake-project. Nevertheless, it has a library component and also has custom -D preprocessing arguments for the build.

Changes

  1. Parsing of compilation databases.
  2. Preprocessing of compilation database command objects, either from command (from CMake) or arguments (from Bear, compiledb).
  3. Output (compilation database) preprocessed files into new .goblint/preprocessed/ subdirectory. Over time we should consolidate all of Goblint's generated data (e.g. incremental_data) there for ease of management instead of scattering our files in top-level directories.
  4. Support for directories to be analyzed, e.g. goblint . for current directory. Looks up compilation database or Makefile in the directory and uses that; doesn't recurse into individual C files because that's extremely unlikely to be correct on any real project.
  5. Change cppflags option from string to string list. This integrates better with command objects with arguments (otherwise we'd have to parse shell commands a la Python's shlex).
  6. autogen support by @stilscher. It can be there although I believe Goblint shouldn't be in charge of configuring the project that it's analyzing (and sometimes you might want to use an alternative configuration instead of the default we currently call). Instead the user should have configured the project as desired (including with CMake) and we analyze just that (e.g. the compilation database or Makefile).

TODO

  • Try on real projects to see if it works.

stilscher and others added 27 commits November 11, 2021 15:24
@sim642
Copy link
Member Author

sim642 commented Nov 15, 2021

I also added support for analyzing directories, e.g. goblint .. This will be useful for GobPie, so it can just call Goblint on the enabled directory instead of duplicating the logic to figure out what (compilation database or Makefile) to use.

@sim642 sim642 merged commit 15da483 into master Nov 23, 2021
@sim642 sim642 deleted the compilation-database branch November 23, 2021 11:23
sim642 added a commit to goblint/action that referenced this pull request Nov 23, 2021
@sim642 sim642 added this to the v2.0.0 milestone Aug 12, 2022
sim642 added a commit to sim642/opam-repository that referenced this pull request Aug 18, 2022
CHANGES:

Goblint "lean" release after a lot of cleanup.

* Remove unmaintained analyses: OSEK, ARINC, shapes, containment, deadlocksByRaces (goblint/analyzer#460, goblint/analyzer#736, goblint/analyzer#812, goblint/analyzer#474).
* Add interactive analysis (goblint/analyzer#391).
* Add server mode (goblint/analyzer#522).
* Add Compilation Database support (goblint/analyzer#406, goblint/analyzer#448).
* Add floating point domain, unrolled array domain and improved struct domains (goblint/analyzer#734, goblint/analyzer#761, goblint/analyzer#577, goblint/analyzer#419).
* Add static loop unrolling and heap variable unrolling (goblint/analyzer#563, goblint/analyzer#722).
* Improve race detection with may-happen-in-parallel analysis (goblint/analyzer#529, goblint/analyzer#518, goblint/analyzer#595).
* Reimplement lockset and deadlock analyses (goblint/analyzer#659, goblint/analyzer#662, goblint/analyzer#650, goblint/analyzer#655).
* Add pthread extraction to Promela (goblint/analyzer#220).
* Add location spans to output (goblint/analyzer#428, goblint/analyzer#449).
* Improve race reporting (goblint/analyzer#550, goblint/analyzer#551).
* Improve dead code reporting (goblint/analyzer#94, goblint/analyzer#353, goblint/analyzer#785).
* Refactor warnings (goblint/analyzer#55, goblint/analyzer#783).
* Add JSON schema for configuration (goblint/analyzer#476, goblint/analyzer#499).
* Refactor option names (goblint/analyzer#28, goblint/analyzer#192, goblint/analyzer#516, goblint/analyzer#675).
* Add bash completion (goblint/analyzer#669).
* Add OCaml 4.13 and 4.14 support, remove OCaml 4.09 support (goblint/analyzer#503, goblint/analyzer#672).
sim642 added a commit to sim642/opam-repository that referenced this pull request Aug 18, 2022
CHANGES:

Goblint "lean" release after a lot of cleanup.

* Remove unmaintained analyses: OSEK, ARINC, shapes, containment, deadlocksByRaces (goblint/analyzer#460, goblint/analyzer#736, goblint/analyzer#812, goblint/analyzer#474).
* Add interactive analysis (goblint/analyzer#391).
* Add server mode (goblint/analyzer#522).
* Add Compilation Database support (goblint/analyzer#406, goblint/analyzer#448).
* Add floating point domain, unrolled array domain and improved struct domains (goblint/analyzer#734, goblint/analyzer#761, goblint/analyzer#577, goblint/analyzer#419).
* Add static loop unrolling and heap variable unrolling (goblint/analyzer#563, goblint/analyzer#722).
* Improve race detection with may-happen-in-parallel analysis (goblint/analyzer#529, goblint/analyzer#518, goblint/analyzer#595).
* Reimplement lockset and deadlock analyses (goblint/analyzer#659, goblint/analyzer#662, goblint/analyzer#650, goblint/analyzer#655).
* Add pthread extraction to Promela (goblint/analyzer#220).
* Add location spans to output (goblint/analyzer#428, goblint/analyzer#449).
* Improve race reporting (goblint/analyzer#550, goblint/analyzer#551).
* Improve dead code reporting (goblint/analyzer#94, goblint/analyzer#353, goblint/analyzer#785).
* Refactor warnings (goblint/analyzer#55, goblint/analyzer#783).
* Add JSON schema for configuration (goblint/analyzer#476, goblint/analyzer#499).
* Refactor option names (goblint/analyzer#28, goblint/analyzer#192, goblint/analyzer#516, goblint/analyzer#675).
* Add bash completion (goblint/analyzer#669).
* Add OCaml 4.13 and 4.14 support, remove OCaml 4.09 support (goblint/analyzer#503, goblint/analyzer#672).
# for free to join this conversation on GitHub. Already have an account? # to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Compilation Database support
3 participants