package goblint
Install
Dune Dependency
Authors
Maintainers
Sources
sha256=99b78e6def71534d195eef9084baa26d8334b36084e120aa6afb300c9bf8afa6
sha512=f3162bd95a03c00358a2991f6152fc6169205bfb4c55e2c483e98cc3935673df9656d025b6f1ea0fa5f1bd0aee037d4f483966b0d2907e3fa9bf11a93a3392af
Description
Goblint is a sound static analysis framework for C programs using abstract interpretation. It specializes in thread-modular verification of multi-threaded programs, especially regarding data races. Goblint includes analyses for assertions, overflows, deadlocks, etc and can be extended with new analyses.
Tags
program analysis program verification static analysis abstract interpretation C data race analysis concurrencyPublished: 06 Aug 2024
README
Goblint
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
Install opam.
Make sure the following are installed:
git
,patch
,m4
,autoconf
,libgmp-dev
,libmpfr-dev
andpkg-config
.Run
make setup
to install OCaml and dependencies via opam.Run
make
to build Goblint itself.Run
make install
to install Goblint into the opam switch for usage via switch'sPATH
.Optional: See
scripts/bash-completion.sh
for setting up bash completion for Goblint arguments.
MacOS
Install GCC with
brew install gcc grep
(first runxcode-select --install
if you don't want to build it from source). Goblint requires GCC while macOS's defaultcpp
is Clang, which will not work.ONLY for M1 (ARM64) processor: homebrew changed its install location from
/usr/local/
to/opt/homebrew/
. For packages to find their dependecies executesudo ln -s /opt/homebrew/{include,lib} /usr/local/
.Continue using Linux instructions (the formulae in brew for
patch
,libgmp-dev
,libmpfr-dev
aregpatch
,gmp
,mpfr
, respectively).
Windows
Install WSL2. Goblint is not compatible with WSL1.
Continue using Linux instructions in WSL.
Other
devcontainer. Select "Reopen in Container" in VS Code and continue with
make
using Linux instructions in devcontainer.Docker (GitHub Container Registry). Run
docker pull ghcr.io/goblint/analyzer:latest
(or:nightly
).Docker (repository). Clone and run
docker build -t goblint .
.Vagrant. Clone and run
vagrant up && vagrant ssh
.
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.
Dependencies (25)
- conf-gcc
-
conf-gmp
>= "3"
- catapult-file
- catapult
- uuidm
-
yaml
>= "3.0.0"
- arg-complete
- cpu
-
fileutils
>= "0.6.4"
-
sha
>= "1.12"
-
jsonrpc
>= "1.12"
- json-data-encoding
- dune-build-info
- dune-site
- fpath
-
ppx_deriving_yojson
>= "3.7.0"
-
ppx_deriving_hash
>= "0.1.2"
-
ppx_deriving
>= "6.0.2"
-
qcheck-core
>= "0.19"
-
yojson
>= "2.0.0"
-
zarith
>= "1.10"
-
batteries
>= "3.5.1"
-
goblint-cil
>= "2.0.4"
-
ocaml
>= "4.14"
-
dune
>= "3.7"
Dev Dependencies (5)
-
benchmark
with-test
-
conf-ruby
with-test
-
odoc
with-doc
-
qcheck-ounit
with-test
-
ounit2
with-test
Used by
None
Conflicts (2)
-
ez-conf-lib
= "1"
-
result
< "1.5"