Skip to content

Commit edf7e6f

Browse files
sim642sim642
committed
Merge branch 'master' into klever
2 parents 1fbf910 + d5163c9 commit edf7e6f

File tree

2,341 files changed

+91466
-32268
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

2,341 files changed

+91466
-32268
lines changed

‎.devcontainer/Dockerfile‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,9 @@
11
# just -opam tag because make setup will install ocaml compiler
2-
FROM ocaml/opam:ubuntu-21.04-opam AS dev
2+
FROM ocaml/opam:ubuntu-22.04-opam AS dev
33

44
# TODO: use opam depext
55
RUN sudo apt-get update \
6-
&& sudo apt-get install -y libgmp-dev libmpfr-dev m4 autoconf pkg-config ruby gem curl
6+
&& sudo apt-get install -y libgmp-dev libmpfr-dev m4 autoconf gcc-multilib pkg-config ruby gem curl
77

88
# remove default Docker <[email protected]> git credentials added by opam base image: https://github.com/avsm/ocaml-dockerfile/blob/f184554282a3836bf3f1c34d20e77d0530f8349d/src-opam/dockerfile_linux.ml#L24-L28
99
# this prevents devcontainer from using outside git credentials: https://code.visualstudio.com/docs/remote/containers#_sharing-git-credentials-with-your-container

‎.git-blame-ignore-revs‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -28,3 +28,6 @@ ec8611a3a72ae0d95ec82ffee16c5c4785111aa1
2828

2929
# Set up end-of-line normalization.
3030
78fd79e7f4d15c4412221b155971fac2e0616b90
31+
32+
# fix indentation in baseInvariant
33+
f3ffd5e45c034574020f56519ccdb021da2a1479

‎.github/workflows/coverage.yml‎

Lines changed: 95 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,95 @@
1+
name: coverage
2+
3+
on:
4+
pull_request:
5+
6+
workflow_dispatch:
7+
8+
schedule:
9+
# nightly
10+
- cron: '31 1 * * *' # 01:31 UTC, 02:31/03:31 Munich, 03:31/04:31 Tartu
11+
# GitHub Actions load is high at minute 0, so avoid that
12+
13+
jobs:
14+
coverage:
15+
strategy:
16+
fail-fast: false
17+
matrix:
18+
os:
19+
- ubuntu-latest
20+
ocaml-compiler:
21+
- ocaml-variants.4.14.0+options,ocaml-option-flambda # matches opam lock file
22+
# don't add any other because they won't be used
23+
24+
runs-on: ${{ matrix.os }}
25+
26+
env:
27+
OCAMLRUNPARAM: b
28+
29+
steps:
30+
- name: Checkout code
31+
uses: actions/checkout@v4
32+
33+
- name: Set up OCaml ${{ matrix.ocaml-compiler }}
34+
env:
35+
# otherwise setup-ocaml pins non-locked dependencies
36+
# https://github.com/ocaml/setup-ocaml/issues/166
37+
OPAMLOCKED: locked
38+
uses: ocaml/setup-ocaml@v2
39+
with:
40+
ocaml-compiler: ${{ matrix.ocaml-compiler }}
41+
42+
- name: Install dependencies
43+
run: opam install . --deps-only --locked --with-test
44+
45+
- name: Install coverage dependencies
46+
run: opam install bisect_ppx
47+
48+
- name: Build
49+
run: ./make.sh coverage
50+
51+
- name: Test regression
52+
run: ./make.sh headers testci
53+
54+
- name: Test apron regression # skipped by default but CI has apron, so explicitly test group (which ignores skipping -- it's now a feature!)
55+
run: |
56+
ruby scripts/update_suite.rb group apron -s
57+
ruby scripts/update_suite.rb group apron2 -s
58+
59+
- name: Test apron octagon regression # skipped by default but CI has apron, so explicitly test group (which ignores skipping -- it's now a feature!)
60+
run: ruby scripts/update_suite.rb group octagon -s
61+
62+
- name: Test apron affeq regression # skipped by default but CI has apron, so explicitly test group (which ignores skipping -- it's now a feature!)
63+
run: ruby scripts/update_suite.rb group affeq -s
64+
65+
- name: Test apron regression (Mukherjee et. al SAS '17 paper') # skipped by default but CI has apron, so explicitly test group (which ignores skipping -- it's now a feature!)
66+
run: ruby scripts/update_suite.rb group apron-mukherjee -s
67+
68+
- name: Test apron termination regression # skipped by default but CI has apron, so explicitly test group (which ignores skipping -- it's now a feature!)
69+
run: ruby scripts/update_suite.rb group termination -s
70+
71+
- name: Test regression cram
72+
run: opam exec -- dune runtest tests/regression
73+
74+
- name: Test incremental cram
75+
run: opam exec -- dune runtest tests/incremental
76+
77+
- name: Test unit
78+
run: opam exec -- dune runtest unittest
79+
80+
- name: Test incremental regression
81+
run: ruby scripts/update_suite.rb -i
82+
83+
- name: Test incremental regression with cfg comparison
84+
run: ruby scripts/update_suite.rb -c
85+
86+
- run: opam exec -- bisect-ppx-report send-to Coveralls --coverage-path=.
87+
env:
88+
COVERALLS_REPO_TOKEN: ${{ secrets.COVERALLS_REPO_TOKEN }}
89+
PULL_REQUEST_NUMBER: ${{ github.event.number }}
90+
91+
- uses: actions/upload-artifact@v3
92+
if: always()
93+
with:
94+
name: suite_result
95+
path: tests/suite_result/

‎.github/workflows/docker.yml‎

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -35,21 +35,21 @@ jobs:
3535

3636
steps:
3737
- name: Checkout code
38-
uses: actions/checkout@v3
38+
uses: actions/checkout@v4
3939

4040
- name: Set up Docker Buildx
41-
uses: docker/setup-buildx-action@v1 # needed for GitHub Actions Cache in build-push-action
41+
uses: docker/setup-buildx-action@v3 # needed for GitHub Actions Cache in build-push-action
4242

4343
- name: Log in to the Container registry
44-
uses: docker/login-action@v1
44+
uses: docker/login-action@v3
4545
with:
4646
registry: ${{ env.REGISTRY }}
4747
username: ${{ github.actor }}
4848
password: ${{ secrets.GITHUB_TOKEN }}
4949

5050
- name: Extract metadata (tags, labels) for Docker
5151
id: meta
52-
uses: docker/metadata-action@v3
52+
uses: docker/metadata-action@v5
5353
with:
5454
images: ${{ env.REGISTRY }}/${{ env.IMAGE_NAME }}
5555
tags: |
@@ -59,7 +59,7 @@ jobs:
5959
6060
- name: Build Docker image
6161
id: build
62-
uses: docker/build-push-action@v2
62+
uses: docker/build-push-action@v5
6363
with:
6464
context: .
6565
load: true # load into docker instead of immediately pushing
@@ -72,7 +72,7 @@ jobs:
7272
run: docker run --rm -v $(pwd):/data ${{ env.REGISTRY }}/${{ env.IMAGE_NAME }}:${{ steps.meta.outputs.version }} /data/tests/regression/04-mutex/01-simple_rc.c # run image by version in case multiple tags
7373

7474
- name: Push Docker image
75-
uses: docker/build-push-action@v2
75+
uses: docker/build-push-action@v5
7676
with:
7777
context: .
7878
push: true

‎.github/workflows/docs.yml‎

Lines changed: 71 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,71 @@
1+
name: docs
2+
3+
on:
4+
push:
5+
branches:
6+
- master
7+
8+
workflow_dispatch:
9+
10+
permissions:
11+
contents: read
12+
pages: write
13+
id-token: write
14+
15+
concurrency:
16+
group: "pages"
17+
cancel-in-progress: true
18+
19+
jobs:
20+
api-build:
21+
strategy:
22+
matrix:
23+
os:
24+
- ubuntu-latest
25+
ocaml-compiler:
26+
- ocaml-variants.4.14.0+options,ocaml-option-flambda # matches opam lock file
27+
# don't add any other because they won't be used
28+
29+
runs-on: ${{ matrix.os }}
30+
31+
steps:
32+
- name: Checkout code
33+
uses: actions/checkout@v4
34+
35+
- name: Check for undocumented modules
36+
run: python scripts/goblint-lib-modules.py
37+
38+
- name: Set up OCaml ${{ matrix.ocaml-compiler }}
39+
env:
40+
# otherwise setup-ocaml pins non-locked dependencies
41+
# https://github.com/ocaml/setup-ocaml/issues/166
42+
OPAMLOCKED: locked
43+
uses: ocaml/setup-ocaml@v2
44+
with:
45+
ocaml-compiler: ${{ matrix.ocaml-compiler }}
46+
47+
- name: Setup Pages
48+
id: pages
49+
uses: actions/configure-pages@v3
50+
51+
- name: Install dependencies
52+
run: opam install . --deps-only --locked --with-doc
53+
54+
- name: Build API docs
55+
run: opam exec -- dune build @doc
56+
57+
- name: Upload artifact
58+
uses: actions/upload-pages-artifact@v2
59+
with:
60+
path: _build/default/_doc/_html/
61+
62+
api-deploy:
63+
environment:
64+
name: github-pages
65+
url: ${{ steps.deployment.outputs.page_url }}
66+
runs-on: ubuntu-latest
67+
needs: api-build
68+
steps:
69+
- name: Deploy to GitHub Pages
70+
id: deployment
71+
uses: actions/deploy-pages@v2

‎.github/workflows/indentation.yml‎

Lines changed: 10 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -1,43 +1,33 @@
11
name: indentation
22

3-
on: [ push, pull_request]
3+
on:
4+
push:
5+
pull_request:
6+
workflow_dispatch:
47

58
jobs:
69
indentation:
7-
strategy: # remove?
10+
strategy:
811
matrix:
912
os:
1013
- ubuntu-latest
1114
ocaml-compiler:
12-
- 4.14.0 # setup-ocaml@v1 does not support 4.14.x for ocaml-version
15+
- 4.14.x
1316

1417
runs-on: ${{ matrix.os }}
1518

16-
if: ${{ github.event.before != '0000000000000000000000000000000000000000' }}
19+
if: ${{ !github.event.forced && github.event.before != '0000000000000000000000000000000000000000' }}
1720

1821
steps:
1922
- name: Checkout code
20-
uses: actions/checkout@v3
23+
uses: actions/checkout@v4
2124
with:
2225
fetch-depth: 0
2326

24-
# reuse tests.yml or depend on it to not have to setup OCaml? https://docs.github.com/en/actions/reference/workflow-syntax-for-github-actions#example-using-an-action-in-the-same-repository-as-the-workflow
25-
26-
# rely on cache for now
27-
- name: Cache opam switch # https://github.com/marketplace/actions/cache
28-
uses: actions/cache@v3
29-
with:
30-
# A list of files, directories, and wildcard patterns to cache and restore
31-
path: |
32-
~/.opam
33-
_opam
34-
# Key for restoring and saving the cache
35-
key: opam-ocp-indent-${{ runner.os }}-${{ matrix.ocaml-compiler }}
36-
3727
- name: Set up OCaml ${{ matrix.ocaml-compiler }}
38-
uses: ocaml/setup-ocaml@v1 # intentionally use v1 instead of v2 because it's faster with manual caching: https://github.com/goblint/analyzer/pull/308#issuecomment-887805857
28+
uses: ocaml/setup-ocaml@v2
3929
with:
40-
ocaml-version: ${{ matrix.ocaml-compiler }}
30+
ocaml-compiler: ${{ matrix.ocaml-compiler }}
4131

4232
- name: Install ocp-indent
4333
run: opam install -y ocp-indent

0 commit comments

Comments
 (0)