search

goblint / analyzer

Static analysis framework for C
https://goblint.in.tum.de
MIT License
184 stars 75 forks source link
abstract-interpretation c ocaml program-analysis race-conditions race-detection software-verification static-analysis static-code-analysis

readme

Goblint

GitHub release status opam package status Zenodo DOI

locked workflow status unlocked workflow status Coverage Status docker workflow status Documentation Status project chat

Documentation can be browsed on Read the Docs or GitHub.

Installing

Both for using an up-to-date version of Goblint or developing it, the best way is to install from source by cloning this repository. For benchmarking Goblint, please follow the Benchmarking guide on Read the Docs.

Linux

  1. Install opam.
  2. Make sure the following are installed: git, patch, m4, autoconf, libgmp-dev, libmpfr-dev and pkg-config.
  3. Run make setup to install OCaml and dependencies via opam.
  4. Run make to build Goblint itself.
  5. Run make install to install Goblint into the opam switch for usage via switch's PATH.
  6. Optional: See scripts/bash-completion.sh for setting up bash completion for Goblint arguments.

MacOS

  1. Install GCC with brew install gcc grep (first run xcode-select --install if you don't want to build it from source). Goblint requires GCC while macOS's default cpp is Clang, which will not work.
  2. ONLY for M1 (ARM64) processor: homebrew changed its install location from /usr/local/ to /opt/homebrew/. For packages to find their dependecies execute sudo ln -s /opt/homebrew/{include,lib} /usr/local/.
  3. Continue using Linux instructions (the formulae in brew for patch, libgmp-dev, libmpfr-dev are gpatch, gmp, mpfr, respectively).

Windows

  1. Install WSL2. Goblint is not compatible with WSL1.
  2. Continue using Linux instructions in WSL.

Other

Running

To confirm that building worked, you can try running Goblint as follows:

./goblint tests/regression/04-mutex/01-simple_rc.c

To confirm that installation into the opam switch worked, you can try running Goblint as follows:

goblint tests/regression/04-mutex/01-simple_rc.c

To confirm that the Docker container worked, you can try running Goblint as follows:

docker run -it --rm -v $(pwd):/data goblint /data/tests/regression/04-mutex/01-simple_rc.c

If pulled from GitHub Container Registry, use the container name ghcr.io/goblint/analyzer:latest (or :nightly) instead.

For further information, see documentation.

Acknowledgements

Work on Goblint was supported in part by Deutsche Forschungsgemeinschaft (DFG) (47140942/1480 PUMA, 378803395/2428 ConVeY), ARTEMIS Joint Undertaking (269335 MBAT), ITEA3 project 14014 ASSUME, the Shota Rustaveli National Science Foundation of Georgia FR-21-7973, the Estonian Research Council (IUT2-1, PSG61), and the Estonian Centre of Excellence in IT (EXCITE), funded by the European Regional Development Fund.

We also thank Zulip for providing free Zulip Cloud Standard hosting for the Goblint project. Zulip is an open-source modern team chat app designed to keep both live and asynchronous conversations organized.