Skip to content

Commit 3b2df23

Browse files
sim642sim642
committed
Merge branch 'master' into threadid-history-may_create
2 parents babbf09 + ea7ee83 commit 3b2df23

File tree

489 files changed

+17095
-8984
lines changed

Some content is hidden

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

489 files changed

+17095
-8984
lines changed

‎.git-blame-ignore-revs‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -37,3 +37,6 @@ c3e2cc848479ae86de5542b6ab0e75a74e9cf8c9
3737

3838
# Fix LibraryFunctions.invalidate_actions indentation
3939
5662024232f32fe74dd25c9317dee4436ecb212d
40+
41+
# Rename ctx -> man
42+
0c155e68607fede6fab17704a9a7aee38df5408e

‎.github/workflows/coverage.yml‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -16,7 +16,7 @@ jobs:
1616
fail-fast: false
1717
matrix:
1818
os:
19-
- ubuntu-latest
19+
- ubuntu-22.04 # https://github.com/ocaml/setup-ocaml/issues/872
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
@@ -40,7 +40,7 @@ jobs:
4040
ocaml-compiler: ${{ matrix.ocaml-compiler }}
4141

4242
- name: Install graph-easy # TODO: remove if depext --with-test works
43-
if: ${{ matrix.os == 'ubuntu-latest' }}
43+
if: ${{ matrix.os == 'ubuntu-22.04' }}
4444
run: sudo apt install -y libgraph-easy-perl
4545

4646
- name: Install dependencies

‎.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-latest
19+
- ubuntu-22.04 # https://github.com/ocaml/setup-ocaml/issues/872
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-latest
13+
- ubuntu-22.04 # https://github.com/ocaml/setup-ocaml/issues/872
1414
ocaml-compiler:
1515
- 4.14.x
1616

‎.github/workflows/locked.yml‎

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -17,7 +17,7 @@ jobs:
1717
fail-fast: false
1818
matrix:
1919
os:
20-
- ubuntu-latest
20+
- ubuntu-22.04 # https://github.com/ocaml/setup-ocaml/issues/872
2121
- macos-13
2222
ocaml-compiler:
2323
- ocaml-variants.4.14.2+options,ocaml-option-flambda # matches opam lock file
@@ -42,7 +42,7 @@ jobs:
4242
ocaml-compiler: ${{ matrix.ocaml-compiler }}
4343

4444
- name: Install graph-easy # TODO: remove if depext --with-test works
45-
if: ${{ matrix.os == 'ubuntu-latest' }}
45+
if: ${{ matrix.os == 'ubuntu-22.04' }}
4646
run: sudo apt install -y libgraph-easy-perl
4747

4848
- name: Install dependencies
@@ -70,7 +70,7 @@ jobs:
7070
fail-fast: false
7171
matrix:
7272
os:
73-
- ubuntu-latest
73+
- ubuntu-22.04 # https://github.com/ocaml/setup-ocaml/issues/872
7474
ocaml-compiler:
7575
- ocaml-variants.4.14.2+options,ocaml-option-flambda # matches opam lock file
7676
# don't add any other because they won't be used
@@ -91,7 +91,7 @@ jobs:
9191
ocaml-compiler: ${{ matrix.ocaml-compiler }}
9292

9393
- name: Install graph-easy # TODO: remove if depext --with-test works
94-
if: ${{ matrix.os == 'ubuntu-latest' }}
94+
if: ${{ matrix.os == 'ubuntu-22.04' }}
9595
run: sudo apt install -y libgraph-easy-perl
9696

9797
- name: Install spin
@@ -112,7 +112,7 @@ jobs:
112112
fail-fast: false
113113
matrix:
114114
os:
115-
- ubuntu-latest
115+
- ubuntu-22.04 # https://github.com/ocaml/setup-ocaml/issues/872
116116
ocaml-compiler:
117117
- ocaml-variants.4.14.2+options,ocaml-option-flambda # matches opam lock file
118118
# don't add any other because they won't be used

‎.github/workflows/unlocked.yml‎

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -15,7 +15,7 @@ jobs:
1515
fail-fast: false
1616
matrix:
1717
os:
18-
- ubuntu-latest
18+
- ubuntu-22.04 # https://github.com/ocaml/setup-ocaml/issues/872
1919
- macos-13
2020
ocaml-compiler:
2121
- 5.2.x
@@ -30,7 +30,7 @@ jobs:
3030
- false
3131

3232
include:
33-
- os: ubuntu-latest
33+
- os: ubuntu-22.04 # https://github.com/ocaml/setup-ocaml/issues/872
3434
ocaml-compiler: 4.14.x
3535
z3: true
3636
- os: macos-latest
@@ -52,7 +52,7 @@ jobs:
5252
ocaml-compiler: ${{ matrix.ocaml-compiler }}
5353

5454
- name: Install graph-easy # TODO: remove if depext --with-test works
55-
if: ${{ matrix.os == 'ubuntu-latest' }}
55+
if: ${{ matrix.os == 'ubuntu-22.04' }}
5656
run: sudo apt install -y libgraph-easy-perl
5757

5858
- name: Install dependencies
@@ -90,7 +90,7 @@ jobs:
9090
fail-fast: false
9191
matrix:
9292
os:
93-
- ubuntu-latest
93+
- ubuntu-22.04 # https://github.com/ocaml/setup-ocaml/issues/872
9494
- macos-13
9595
ocaml-compiler:
9696
- ocaml-variants.4.14.2+options,ocaml-option-flambda # matches opam lock file, downgrade deps step
@@ -112,7 +112,7 @@ jobs:
112112
ocaml-compiler: ${{ matrix.ocaml-compiler }}
113113

114114
- name: Install graph-easy # TODO: remove if depext --with-test works
115-
if: ${{ matrix.os == 'ubuntu-latest' }}
115+
if: ${{ matrix.os == 'ubuntu-22.04' }}
116116
run: sudo apt install -y libgraph-easy-perl
117117

118118
- name: Install dependencies
@@ -187,7 +187,7 @@ jobs:
187187
fail-fast: false
188188
matrix:
189189
os:
190-
- ubuntu-latest
190+
- ubuntu-22.04 # https://github.com/ocaml/setup-ocaml/issues/872
191191
- macos-13
192192
ocaml-compiler:
193193
- ocaml-variants.4.14.2+options,ocaml-option-flambda # matches opam lock file
@@ -204,7 +204,7 @@ jobs:
204204
ocaml-compiler: ${{ matrix.ocaml-compiler }}
205205

206206
- name: Install graph-easy # TODO: remove if depext --with-test works
207-
if: ${{ matrix.os == 'ubuntu-latest' }}
207+
if: ${{ matrix.os == 'ubuntu-22.04' }}
208208
run: sudo apt install -y libgraph-easy-perl
209209

210210
- name: Install Goblint with test

‎.semgrep/fold.yml‎

Lines changed: 26 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,26 @@
1+
rules:
2+
- id: fold-exists
3+
patterns:
4+
- pattern-either:
5+
- pattern: $D.fold ... false
6+
- pattern: $D.fold_left ... false
7+
- pattern: $D.fold_right ... false
8+
- pattern: fold ... false
9+
- pattern: fold_left ... false
10+
- pattern: fold_right ... false
11+
message: consider replacing fold with exists
12+
languages: [ocaml]
13+
severity: WARNING
14+
15+
- id: fold-for_all
16+
patterns:
17+
- pattern-either:
18+
- pattern: $D.fold ... true
19+
- pattern: $D.fold_left ... true
20+
- pattern: $D.fold_right ... true
21+
- pattern: fold ... true
22+
- pattern: fold_left ... true
23+
- pattern: fold_right ... true
24+
message: consider replacing fold with for_all
25+
languages: [ocaml]
26+
severity: WARNING

‎.semgrep/tracing.yml‎

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -8,8 +8,16 @@ rules:
88
- pattern: Messages.tracec
99
- pattern: Messages.traceu
1010
- pattern: Messages.traceli
11+
- pattern: M.trace
12+
- pattern: M.tracel
13+
- pattern: M.tracei
14+
- pattern: M.tracec
15+
- pattern: M.traceu
16+
- pattern: M.traceli
1117
- pattern-not-inside: if Messages.tracing then ...
1218
- pattern-not-inside: if Messages.tracing && ... then ...
19+
- pattern-not-inside: if M.tracing then ...
20+
- pattern-not-inside: if M.tracing && ... then ...
1321
message: trace functions should only be called if tracing is enabled at compile time
1422
languages: [ocaml]
1523
severity: WARNING

‎CHANGELOG.md‎

Lines changed: 12 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,14 @@
1+
## v2.5.0
2+
Functionally equivalent to Goblint in SV-COMP 2025.
3+
4+
* Add 32bit vs 64bit architecture support (#54, #1574).
5+
* Add per-function context gas analysis (#1569, #1570, #1598).
6+
* Adapt automatic static loop unrolling (#1516, #1582, #1583, #1584, #1590, #1595, #1599).
7+
* Adapt automatic configuration tuning (#1450, #1612, #1181, #1604).
8+
* Simplify non-relational integer invariants in witnesses (#1517).
9+
* Fix excessive hash collisions (#1594, #1602).
10+
* Clean up various code (#1095, #1523, #1554, #1575, #1588, #1597, #1614).
11+
112
## v2.4.0
213
* Remove unmaintained analyses: spec, file (#1281).
314
* Add linear two-variable equalities analysis (#1297, #1412, #1466).
@@ -10,7 +21,7 @@
1021
* Fix mutex type analysis unsoundness and enable it by default (#1414, #1416, #1510).
1122
* Add points-to set refinement on mutex path splitting (#1287, #1343, #1374, #1396, #1407).
1223
* Improve narrowing operators (#1502, #1540, #1543).
13-
* Extract automatic configuration tuning for soundness (#1369).
24+
* Extract automatic configuration tuning for soundness (#1469).
1425
* Fix many locations in witnesses (#1355, #1372, #1400, #1403).
1526
* Improve output readability (#1294, #1312, #1405, #1497).
1627
* Refactor logging (#1117).

‎conf/svcomp-ghost.json‎

Lines changed: 139 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,139 @@
1+
{
2+
"ana": {
3+
"sv-comp": {
4+
"enabled": true,
5+
"functions": true
6+
},
7+
"int": {
8+
"def_exc": true,
9+
"enums": false,
10+
"interval": true
11+
},
12+
"float": {
13+
"interval": true,
14+
"evaluate_math_functions": true
15+
},
16+
"activated": [
17+
"base",
18+
"threadid",
19+
"threadflag",
20+
"threadreturn",
21+
"mallocWrapper",
22+
"mutexEvents",
23+
"mutex",
24+
"access",
25+
"race",
26+
"escape",
27+
"expRelation",
28+
"mhp",
29+
"assert",
30+
"var_eq",
31+
"symb_locks",
32+
"region",
33+
"thread",
34+
"threadJoins",
35+
"abortUnless",
36+
"mutexGhosts",
37+
"pthreadMutexType"
38+
],
39+
"path_sens": [
40+
"mutex",
41+
"malloc_null",
42+
"uninit",
43+
"expsplit",
44+
"activeSetjmp",
45+
"memLeak",
46+
"threadflag"
47+
],
48+
"context": {
49+
"widen": false
50+
},
51+
"base": {
52+
"arrays": {
53+
"domain": "partitioned"
54+
},
55+
"invariant": {
56+
"local": false,
57+
"global": true
58+
}
59+
},
60+
"relation": {
61+
"invariant": {
62+
"local": false,
63+
"global": true,
64+
"one-var": false
65+
}
66+
},
67+
"apron": {
68+
"invariant": {
69+
"diff-box": true
70+
}
71+
},
72+
"var_eq": {
73+
"invariant": {
74+
"enabled": false
75+
}
76+
},
77+
"race": {
78+
"free": false,
79+
"call": false
80+
},
81+
"autotune": {
82+
"enabled": true,
83+
"activated": [
84+
"singleThreaded",
85+
"mallocWrappers",
86+
"noRecursiveIntervals",
87+
"enums",
88+
"congruence",
89+
"octagon",
90+
"wideningThresholds",
91+
"loopUnrollHeuristic",
92+
"memsafetySpecification",
93+
"noOverflows",
94+
"termination",
95+
"tmpSpecialAnalysis"
96+
]
97+
}
98+
},
99+
"exp": {
100+
"region-offsets": true
101+
},
102+
"solver": "td3",
103+
"sem": {
104+
"unknown_function": {
105+
"spawn": false
106+
},
107+
"int": {
108+
"signed_overflow": "assume_none"
109+
},
110+
"null-pointer": {
111+
"dereference": "assume_none"
112+
}
113+
},
114+
"witness": {
115+
"graphml": {
116+
"enabled": false
117+
},
118+
"yaml": {
119+
"enabled": true,
120+
"format-version": "2.1",
121+
"entry-types": [
122+
"flow_insensitive_invariant",
123+
"ghost_instrumentation"
124+
]
125+
},
126+
"invariant": {
127+
"loop-head": true,
128+
"after-lock": true,
129+
"other": true,
130+
"accessed": false,
131+
"exact": true,
132+
"all-locals": false,
133+
"flow_insensitive-as": "invariant_set-location_invariant"
134+
}
135+
},
136+
"pre": {
137+
"enabled": false
138+
}
139+
}

0 commit comments

Comments
 (0)