Skip to content

Commit 8688982

Browse files
sim642sim642
committed
Merge branch 'master' into div-by-zero-invariant
2 parents c4b2874 + 762b284 commit 8688982

174 files changed

Lines changed: 4455 additions & 1301 deletions

File tree

Some content is hidden

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

‎.github/workflows/coverage.yml‎

Lines changed: 5 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,8 @@ name: coverage
22

33
on:
44
pull_request:
5+
paths-ignore:
6+
- 'docs/**'
57

68
workflow_dispatch:
79

@@ -16,7 +18,7 @@ jobs:
1618
fail-fast: false
1719
matrix:
1820
os:
19-
- ubuntu-22.04 # https://github.com/ocaml/setup-ocaml/issues/872
21+
- ubuntu-latest
2022
ocaml-compiler:
2123
- ocaml-variants.4.14.2+options,ocaml-option-flambda # matches opam lock file
2224
# don't add any other because they won't be used
@@ -40,7 +42,7 @@ jobs:
4042
ocaml-compiler: ${{ matrix.ocaml-compiler }}
4143

4244
- name: Install graph-easy # TODO: remove if depext --with-test works (https://github.com/ocaml/opam/issues/5836)
43-
if: ${{ matrix.os == 'ubuntu-22.04' }}
45+
if: ${{ startsWith(matrix.os, 'ubuntu') }}
4446
run: sudo apt install -y libgraph-easy-perl
4547

4648
- name: Install dependencies
@@ -70,7 +72,7 @@ jobs:
7072
COVERALLS_REPO_TOKEN: ${{ secrets.COVERALLS_REPO_TOKEN }}
7173
PULL_REQUEST_NUMBER: ${{ github.event.number }}
7274

73-
- uses: actions/upload-artifact@v5
75+
- uses: actions/upload-artifact@v7
7476
if: always()
7577
with:
7678
name: suite_result

‎.github/workflows/docker.yml‎

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -38,18 +38,18 @@ jobs:
3838
uses: actions/checkout@v6
3939

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

4343
- name: Log in to the Container registry
44-
uses: docker/login-action@v3
44+
uses: docker/login-action@v4
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@v5
52+
uses: docker/metadata-action@v6
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@v6
62+
uses: docker/build-push-action@v7
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@v6
75+
uses: docker/build-push-action@v7
7676
with:
7777
context: .
7878
push: true

‎.github/workflows/docs.yml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -16,7 +16,7 @@ jobs:
1616
strategy:
1717
matrix:
1818
os:
19-
- ubuntu-22.04 # https://github.com/ocaml/setup-ocaml/issues/872
19+
- ubuntu-latest
2020
ocaml-compiler:
2121
- ocaml-variants.4.14.2+options,ocaml-option-flambda # matches opam lock file
2222
# don't add any other because they won't be used

‎.github/workflows/indentation.yml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,7 @@ jobs:
1010
strategy:
1111
matrix:
1212
os:
13-
- ubuntu-22.04 # https://github.com/ocaml/setup-ocaml/issues/872
13+
- ubuntu-latest
1414
ocaml-compiler:
1515
- 4.14.x
1616

‎.github/workflows/locked.yml‎

Lines changed: 10 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,11 @@ name: locked
22

33
on:
44
push:
5+
paths-ignore:
6+
- 'docs/**'
57
pull_request:
8+
paths-ignore:
9+
- 'docs/**'
610

711
workflow_dispatch:
812

@@ -17,8 +21,8 @@ jobs:
1721
fail-fast: false
1822
matrix:
1923
os:
20-
- ubuntu-22.04 # https://github.com/ocaml/setup-ocaml/issues/872
21-
- macos-13
24+
- ubuntu-latest
25+
- macos-latest
2226
ocaml-compiler:
2327
- ocaml-variants.4.14.2+options,ocaml-option-flambda # matches opam lock file
2428
# don't add any other because they won't be used
@@ -42,7 +46,7 @@ jobs:
4246
ocaml-compiler: ${{ matrix.ocaml-compiler }}
4347

4448
- name: Install graph-easy # TODO: remove if depext --with-test works (https://github.com/ocaml/opam/issues/5836)
45-
if: ${{ matrix.os == 'ubuntu-22.04' }}
49+
if: ${{ startsWith(matrix.os, 'ubuntu') }}
4650
run: sudo apt install -y libgraph-easy-perl
4751

4852
- name: Install dependencies
@@ -60,7 +64,7 @@ jobs:
6064
- name: Test
6165
run: opam exec -- dune runtest
6266

63-
- uses: actions/upload-artifact@v5
67+
- uses: actions/upload-artifact@v7
6468
if: always()
6569
with:
6670
name: suite_result-${{ matrix.os }}
@@ -73,7 +77,7 @@ jobs:
7377
fail-fast: false
7478
matrix:
7579
os:
76-
- ubuntu-22.04 # https://github.com/ocaml/setup-ocaml/issues/872
80+
- ubuntu-latest
7781
ocaml-compiler:
7882
- ocaml-variants.4.14.2+options,ocaml-option-flambda # matches opam lock file
7983
# don't add any other because they won't be used
@@ -94,7 +98,7 @@ jobs:
9498
ocaml-compiler: ${{ matrix.ocaml-compiler }}
9599

96100
- name: Install graph-easy # TODO: remove if depext --with-test works (https://github.com/ocaml/opam/issues/5836)
97-
if: ${{ matrix.os == 'ubuntu-22.04' }}
101+
if: ${{ startsWith(matrix.os, 'ubuntu') }}
98102
run: sudo apt install -y libgraph-easy-perl
99103

100104
- name: Install spin

‎.github/workflows/unlocked.yml‎

Lines changed: 75 additions & 29 deletions
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,8 @@ name: unlocked
22

33
on:
44
# pull_request: # save CI time on PRs, run manually if needed (before merge) or find out failures from scheduled run (after merge)
5+
# paths-ignore:
6+
# - 'docs/**'
57
workflow_dispatch:
68

79
schedule:
@@ -14,27 +16,71 @@ jobs:
1416
strategy:
1517
fail-fast: false
1618
matrix:
17-
os:
18-
- ubuntu-22.04 # https://github.com/ocaml/setup-ocaml/issues/872
19-
- macos-13
20-
ocaml-compiler:
21-
- 5.2.x
22-
- 5.1.x
23-
- 5.0.x
24-
- ocaml-variants.4.14.2+options,ocaml-option-flambda
25-
- 4.14.x
26-
apron:
27-
- false
28-
- true
29-
z3:
30-
- false
31-
19+
# We don't want a full matrix because it is too slow, so we only have linear axes overriding these below.
3220
include:
33-
- os: ubuntu-22.04 # https://github.com/ocaml/setup-ocaml/issues/872
21+
# Common configuration
22+
- os: ubuntu-24.04
23+
ocaml-compiler: ocaml-variants.4.14.2+options,ocaml-option-flambda # matches opam lock file
24+
apron: true
25+
z3: false
26+
27+
# OCaml versions
28+
- os: ubuntu-24.04
29+
ocaml-compiler: 5.4.x
30+
apron: true
31+
z3: false
32+
- os: ubuntu-24.04
33+
ocaml-compiler: 5.3.x
34+
apron: true
35+
z3: false
36+
- os: ubuntu-24.04
37+
ocaml-compiler: 5.2.x
38+
apron: true
39+
z3: false
40+
- os: ubuntu-24.04
41+
ocaml-compiler: 5.1.x
42+
apron: true
43+
z3: false
44+
- os: ubuntu-24.04
45+
ocaml-compiler: 5.0.x
46+
apron: true
47+
z3: false
48+
- os: ubuntu-24.04
3449
ocaml-compiler: 4.14.x
50+
apron: true
51+
z3: false
52+
53+
# OS-s
54+
- os: ubuntu-22.04
55+
ocaml-compiler: ocaml-variants.4.14.2+options,ocaml-option-flambda # matches opam lock file
56+
apron: true
57+
z3: false
58+
- os: macos-26
59+
ocaml-compiler: ocaml-variants.4.14.2+options,ocaml-option-flambda # matches opam lock file
60+
apron: true
61+
z3: false
62+
- os: macos-15-intel
63+
ocaml-compiler: ocaml-variants.4.14.2+options,ocaml-option-flambda # matches opam lock file
64+
apron: true
65+
z3: false
66+
- os: macos-15
67+
ocaml-compiler: ocaml-variants.4.14.2+options,ocaml-option-flambda # matches opam lock file
68+
apron: true
69+
z3: false
70+
- os: macos-14
71+
ocaml-compiler: ocaml-variants.4.14.2+options,ocaml-option-flambda # matches opam lock file
72+
apron: true
73+
z3: false
74+
75+
# Optional dependencies
76+
- os: ubuntu-24.04
77+
ocaml-compiler: ocaml-variants.4.14.2+options,ocaml-option-flambda # matches opam lock file
78+
apron: false
79+
z3: false
80+
- os: ubuntu-24.04
81+
ocaml-compiler: ocaml-variants.4.14.2+options,ocaml-option-flambda # matches opam lock file
82+
apron: true
3583
z3: true
36-
- os: macos-latest
37-
ocaml-compiler: 4.14.x
3884

3985
# customize name to use readable string for apron instead of just a boolean
4086
# workaround for missing ternary operator: https://github.com/actions/runner/issues/409
@@ -52,7 +98,7 @@ jobs:
5298
ocaml-compiler: ${{ matrix.ocaml-compiler }}
5399

54100
- name: Install graph-easy # TODO: remove if depext --with-test works (https://github.com/ocaml/opam/issues/5836)
55-
if: ${{ matrix.os == 'ubuntu-22.04' }}
101+
if: ${{ startsWith(matrix.os, 'ubuntu') }}
56102
run: sudo apt install -y libgraph-easy-perl
57103

58104
- name: Install dependencies
@@ -63,7 +109,7 @@ jobs:
63109

64110
- name: Install Apron dependencies
65111
if: ${{ matrix.apron }}
66-
run: opam install apron mlgmpidl.1.2.15
112+
run: opam install apron mlgmpidl
67113

68114
- name: Install Z3 dependencies
69115
if: ${{ matrix.z3 }}
@@ -86,8 +132,8 @@ jobs:
86132
fail-fast: false
87133
matrix:
88134
os:
89-
- ubuntu-22.04 # https://github.com/ocaml/setup-ocaml/issues/872
90-
- macos-13
135+
- ubuntu-latest
136+
- macos-latest
91137
ocaml-compiler:
92138
- ocaml-variants.4.14.2+options,ocaml-option-flambda # matches opam lock file
93139

@@ -105,7 +151,7 @@ jobs:
105151
ocaml-compiler: ${{ matrix.ocaml-compiler }}
106152

107153
- name: Install graph-easy # TODO: remove if depext --with-test works (https://github.com/ocaml/opam/issues/5836)
108-
if: ${{ matrix.os == 'ubuntu-22.04' }}
154+
if: ${{ startsWith(matrix.os, 'ubuntu') }}
109155
run: sudo apt install -y libgraph-easy-perl
110156

111157
- name: Install dependencies
@@ -115,7 +161,7 @@ jobs:
115161
run: sudo gem install os
116162

117163
- name: Install Apron dependencies
118-
run: opam install apron mlgmpidl.1.2.15
164+
run: opam install apron mlgmpidl
119165

120166
- name: Downgrade dependencies
121167
# without "+removed" in criteria, because it also removes optional apron
@@ -138,8 +184,8 @@ jobs:
138184
fail-fast: false
139185
matrix:
140186
os:
141-
- ubuntu-22.04 # https://github.com/ocaml/setup-ocaml/issues/872
142-
- macos-13
187+
- ubuntu-latest
188+
- macos-latest
143189
ocaml-compiler:
144190
- ocaml-variants.4.14.2+options,ocaml-option-flambda # matches opam lock file
145191

@@ -155,14 +201,14 @@ jobs:
155201
ocaml-compiler: ${{ matrix.ocaml-compiler }}
156202

157203
- name: Install graph-easy # TODO: remove if depext --with-test works (https://github.com/ocaml/opam/issues/5836)
158-
if: ${{ matrix.os == 'ubuntu-22.04' }}
204+
if: ${{ startsWith(matrix.os, 'ubuntu') }}
159205
run: sudo apt install -y libgraph-easy-perl
160206

161207
- name: Install Goblint with test
162208
run: opam install goblint --with-test
163209

164210
- name: Install Apron dependencies
165-
run: opam install apron mlgmpidl.1.2.15
211+
run: opam install apron mlgmpidl
166212

167213
- name: Symlink installed goblint to repository # because tests want to use locally built one
168214
run: ln -s $(opam exec -- which goblint) goblint
@@ -206,7 +252,7 @@ jobs:
206252
fail-fast: false
207253
matrix:
208254
os:
209-
- ubuntu-22.04 # https://github.com/ocaml/setup-ocaml/issues/872
255+
- ubuntu-latest
210256
ocaml-compiler:
211257
- ocaml-variants.5.0.0+options,ocaml-option-flambda
212258
node-version:

‎.gitignore‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -91,6 +91,9 @@ gobview_out/*
9191
witness.yml
9292
witness.certificate.yml
9393

94+
# checks
95+
checks.json
96+
9497
# transformations
9598
transformed.c
9699

‎.semgrep/intDomain.yml‎

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
rules:
2+
- id: intDomain-to_int-equal
3+
pattern-either:
4+
- pattern: ID.to_int $X = Some $Y
5+
- pattern: $X |> ID.to_int = Some $Y # Fix doesn't add correct parentheses
6+
- pattern: GobOption.exists (Z.equal $Y) (ID.to_int $X)
7+
fix: ID.equal_to $Y $X = `Eq
8+
message: use dedicated and optimized function instead
9+
languages: [ocaml]
10+
severity: WARNING

‎.semgrep/let.yml‎

Lines changed: 7 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,8 @@
11
rules:
2-
- id: let-unit-in
3-
pattern: let () = $E in ...
4-
message: use ; instead (and, if needed, add surrounding parentheses to preserve precedence)
5-
languages: [ocaml]
6-
severity: WARNING
2+
[]
3+
# TODO: disabled because semgrep cannot distinguish from let@ which is fine (https://github.com/semgrep/semgrep/issues/11432)
4+
# - id: let-unit-in
5+
# pattern: let () = $E in ...
6+
# message: use ; instead (and, if needed, add surrounding parentheses to preserve precedence)
7+
# languages: [ocaml]
8+
# severity: WARNING

0 commit comments

Comments
 (0)