Skip to content
Draft
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
72 commits
Select commit Hold shift + click to select a range
2fb5390
First steps
michael-schwarz Dec 24, 2024
29a3900
Record capacity
michael-schwarz Dec 24, 2024
60c1d72
Add first checks
michael-schwarz Dec 24, 2024
041e544
Use MHP information
michael-schwarz Dec 24, 2024
db320ae
More involved MHP check
michael-schwarz Dec 24, 2024
8b2ede3
Rm spurious variable
michael-schwarz Dec 24, 2024
f418b00
Document pthread barriers
michael-schwarz Dec 24, 2024
93b7f0c
Add `NOMAC` option
michael-schwarz Dec 25, 2024
a990b5f
Remark that `os` gem is needed
michael-schwarz Dec 25, 2024
27dd030
Make sound for multiprocess
michael-schwarz Dec 25, 2024
24d61c0
Fix indentation
michael-schwarz Dec 25, 2024
8fe2e16
Also consider locks
michael-schwarz Dec 25, 2024
05d2f60
Minimal race handling
michael-schwarz Dec 25, 2024
1b3a0d8
Fix pairwise MHP check
michael-schwarz Dec 25, 2024
7e98213
Add case for more waiters
michael-schwarz Dec 25, 2024
1b4beae
Get rid of overcomplicated logic
michael-schwarz Dec 25, 2024
1bfb985
Cleanup
michael-schwarz Dec 25, 2024
7be6d3a
Merge branch 'master' into issue_1651
michael-schwarz Jan 17, 2025
35bec2d
Fix `List.length` call
michael-schwarz Jan 17, 2025
ea90d39
Add first handling to constraints
michael-schwarz Jan 24, 2025
383ad94
Fix failing test
michael-schwarz Jan 24, 2025
ff411e4
More events & constraints
michael-schwarz Jan 24, 2025
8fff9a5
Onces
michael-schwarz Jan 24, 2025
ab0a9db
Refine
michael-schwarz Jan 24, 2025
e255c60
Document `pthread_once`
michael-schwarz Jan 24, 2025
6df3ff8
Add race checking
michael-schwarz Jan 24, 2025
46d4904
Add further example
michael-schwarz Jan 27, 2025
e31ce2a
Only print onces in race info if one of the sets is non-empty
michael-schwarz Jan 27, 2025
9dae404
Further test
michael-schwarz Jan 27, 2025
010380e
Remove workaround for #547
michael-schwarz Jan 27, 2025
aa68509
Use Seq instead of constructing from scratch
michael-schwarz Jan 29, 2025
cb2c858
Merge branch 'issue_1651' into race_digest_staging
michael-schwarz Jan 29, 2025
5c26909
Merge branch 'issue_1662' into race_digest_staging
michael-schwarz Jan 29, 2025
31323cd
Add switch to not use mutexes in race detection
michael-schwarz Jan 30, 2025
d9bd9ca
Add option to disable thread digest
michael-schwarz Jan 30, 2025
164e0c9
Add option for freshness
michael-schwarz Jan 30, 2025
7ae5e07
Add toggle for region / symbLocks
michael-schwarz Jan 30, 2025
1273af2
Thread flag option
michael-schwarz Jan 31, 2025
aa97679
Add `tid` and `joins` digest
michael-schwarz Jan 31, 2025
953577c
Merge branch 'issue_1664' into race_digest_staging
michael-schwarz Jan 31, 2025
4c2d8a3
Add configs for experiments
michael-schwarz Jan 31, 2025
cea4416
Add two more configs
michael-schwarz Jan 31, 2025
4f10b6e
Add full+once+barrier
michael-schwarz May 19, 2025
e461572
Add tid+thread
michael-schwarz May 20, 2025
b8a9baf
Add tf-only config
michael-schwarz May 21, 2025
db51b7e
tf+thread
michael-schwarz May 21, 2025
00ba5a2
Always emit singel-threaded
michael-schwarz May 21, 2025
c22f20b
Add new configs
michael-schwarz May 22, 2025
69cc287
Add config
michael-schwarz May 22, 2025
96d1dab
Always record accesses for race checking
michael-schwarz May 27, 2025
a841507
Remove thread
michael-schwarz May 28, 2025
46aeaa1
Push
michael-schwarz May 28, 2025
6c0f9fd
TID+Join
michael-schwarz May 28, 2025
bc4b34c
Add tests
michael-schwarz May 31, 2025
52e7660
Make setup less strict
michael-schwarz Sep 11, 2025
594757d
Rename general README
michael-schwarz Sep 11, 2025
c4e6f73
Rm test problematic because of preprocessing
michael-schwarz Sep 11, 2025
074734e
Getting started on a README
michael-schwarz Sep 11, 2025
1fa5b4f
Artifacting
michael-schwarz Sep 12, 2025
3c5383b
Progress on README
michael-schwarz Sep 12, 2025
c86fa36
Explanation
michael-schwarz Sep 12, 2025
8efd3bb
Extending & Reusing
michael-schwarz Sep 15, 2025
0466999
Progress
michael-schwarz Sep 15, 2025
8871990
Progress on reproduction
michael-schwarz Sep 15, 2025
24aabcf
explanation
michael-schwarz Sep 15, 2025
1ce8bf5
README
michael-schwarz Sep 15, 2025
41a700c
Remark on QWERTY keyboards
michael-schwarz Sep 16, 2025
6c7f9c9
Relax timing constraints
michael-schwarz Sep 16, 2025
47ce8fa
Typo, commenting out
michael-schwarz Sep 16, 2025
5e79834
Typo
michael-schwarz Sep 16, 2025
8383f03
Unzip necessary
michael-schwarz Sep 16, 2025
e371abb
License remark
michael-schwarz Sep 16, 2025
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 3 additions & 0 deletions .github/workflows/coverage.yml
Original file line number Diff line number Diff line change
Expand Up @@ -46,6 +46,9 @@ jobs:
- name: Install dependencies
run: opam install . --deps-only --locked --with-test

- name: Install os gem for operating system detection
run: sudo gem install os

- name: Install coverage dependencies
run: opam install bisect_ppx

Expand Down
3 changes: 3 additions & 0 deletions .github/workflows/docs.yml
Original file line number Diff line number Diff line change
Expand Up @@ -46,6 +46,9 @@ jobs:
- name: Install dependencies
run: opam install . --deps-only --locked --with-doc

- name: Install os gem for operating system detection
run: sudo gem install os

- name: Build API docs
run: opam exec -- dune build @doc

Expand Down
9 changes: 9 additions & 0 deletions .github/workflows/locked.yml
Original file line number Diff line number Diff line change
Expand Up @@ -48,6 +48,9 @@ jobs:
- name: Install dependencies
run: opam install . --deps-only --locked --with-test

- name: Install os gem for operating system detection
run: sudo gem install os

- name: Build
run: ./make.sh nat

Expand Down Expand Up @@ -100,6 +103,9 @@ jobs:
- name: Install dependencies
run: opam install . --deps-only --locked --with-test

- name: Install os gem for operating system detection
run: sudo gem install os

- name: Build
run: ./make.sh nat

Expand Down Expand Up @@ -142,6 +148,9 @@ jobs:
- name: Install dependencies
run: opam install . --deps-only --locked

- name: Install os gem for operating system detection
run: sudo gem install os

- name: Setup Gobview
run: ./make.sh setup_gobview

Expand Down
6 changes: 6 additions & 0 deletions .github/workflows/unlocked.yml
Original file line number Diff line number Diff line change
Expand Up @@ -57,6 +57,9 @@ jobs:

- name: Install dependencies
run: opam install . --deps-only --with-test

- name: Install os gem for operating system detection
run: sudo gem install os

- name: Install Apron dependencies
if: ${{ matrix.apron }}
Expand Down Expand Up @@ -118,6 +121,9 @@ jobs:
- name: Install dependencies
run: opam install . --deps-only --with-test

- name: Install os gem for operating system detection
run: sudo gem install os

- name: Install Apron dependencies
run: |
opam depext apron
Expand Down
1 change: 1 addition & 0 deletions .gitignore
Original file line number Diff line number Diff line change
Expand Up @@ -23,6 +23,7 @@ doclist.odocl
autom4te.cache
mytests
result/*
results/*
pml-result/*
tests/regression/*/goblint_temp
linux-headers
Expand Down
67 changes: 67 additions & 0 deletions GOBLINT_README.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,67 @@
**This is the README for the entire Goblint system, when getting started with the artifact, it is best to look at README.md**

# Goblint
[![GitHub release status](https://img.shields.io/github/v/release/goblint/analyzer)](https://github.com/goblint/analyzer/releases)
[![opam package status](https://badgen.net/opam/v/goblint)](https://opam.ocaml.org/packages/goblint)
[![Zenodo DOI](https://zenodo.org/badge/2066905.svg)](https://zenodo.org/badge/latestdoi/2066905)

[![locked workflow status](https://github.com/goblint/analyzer/actions/workflows/locked.yml/badge.svg)](https://github.com/goblint/analyzer/actions/workflows/locked.yml)
[![unlocked workflow status](https://github.com/goblint/analyzer/actions/workflows/unlocked.yml/badge.svg)](https://github.com/goblint/analyzer/actions/workflows/unlocked.yml)
[![Coverage Status](https://coveralls.io/repos/github/goblint/analyzer/badge.svg?branch=master)](https://coveralls.io/github/goblint/analyzer?branch=master)
[![docker workflow status](https://github.com/goblint/analyzer/actions/workflows/docker.yml/badge.svg)](https://github.com/goblint/analyzer/actions/workflows/docker.yml)
[![Documentation Status](https://readthedocs.org/projects/goblint/badge/?version=latest)](https://goblint.readthedocs.io/en/latest/?badge=latest)
[![project chat](https://img.shields.io/badge/zulip-join_chat-brightgreen.svg)](https://goblint.zulipchat.com)

Documentation can be browsed on [Read the Docs](https://goblint.readthedocs.io/en/latest/) or [GitHub](./docs/).

## 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](https://goblint.readthedocs.io/en/latest/user-guide/benchmarking/).

### Linux
1. Install [opam](https://opam.ocaml.org/doc/Install.html).
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`](./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](https://docs.microsoft.com/en-us/windows/wsl/install-win10). Goblint is not compatible with WSL1.
2. Continue using Linux instructions in WSL.

### Other
* **[opam](https://opam.ocaml.org/packages/goblint/)**. Install [opam](https://opam.ocaml.org/doc/Install.html) and run `opam install goblint`.
* **[devcontainer](./.devcontainer/).** Select "Reopen in Container" in VS Code and continue with `make` using Linux instructions in devcontainer.
* **[Docker (GitHub Container Registry)](https://github.com/goblint/analyzer/pkgs/container/analyzer)**. 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](https://goblint.readthedocs.io/en/latest/user-guide/running/).

## Acknowledgements

Work on Goblint was supported in part by Deutsche Forschungsgemeinschaft (DFG) (47140942/1480 [PUMA](https://gepris.dfg.de/gepris/projekt/4714094), 378803395/2428 [ConVeY](http://convey.in.tum.de)), ARTEMIS Joint Undertaking (269335 [MBAT](http://www.mbat-artemis.eu/home/)), ITEA3 project 14014 [ASSUME](http://assume-project.eu/), the Shota Rustaveli National Science Foundation of Georgia [FR-21-7973](https://viam.science.tsu.ge/new/index.php?lang=eng&page=projects&subpage=111), the Estonian Research Council ([IUT2-1](https://www.etis.ee/Portal/Projects/Display/561b7b1d-d1dd-43a2-90e5-0661de823823?lang=ENG), [PSG61](https://www.etis.ee/Portal/Projects/Display/743243bb-15c2-47b3-9c10-e7d86a9a276d?lang=ENG)), and the Estonian Centre of Excellence in IT (EXCITE), funded by the European Regional Development Fund.

We also thank [Zulip](https://zulip.com) 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.
Loading
Loading