Skip to content

Commit 8335cae

Browse files
jerhardjerhard
committed
Merge with master.
2 parents ebd90ba + 6e79c1f commit 8335cae

File tree

348 files changed

+6150
-5634
lines changed

Some content is hidden

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

348 files changed

+6150
-5634
lines changed

‎.github/workflows/coverage.yml

+1-1
Original file line numberDiff line numberDiff line change
@@ -88,7 +88,7 @@ jobs:
8888
COVERALLS_REPO_TOKEN: ${{ secrets.COVERALLS_REPO_TOKEN }}
8989
PULL_REQUEST_NUMBER: ${{ github.event.number }}
9090

91-
- uses: actions/upload-artifact@v3
91+
- uses: actions/upload-artifact@v4
9292
if: always()
9393
with:
9494
name: suite_result

‎.github/workflows/docs.yml

+2-2
Original file line numberDiff line numberDiff line change
@@ -46,7 +46,7 @@ jobs:
4646

4747
- name: Setup Pages
4848
id: pages
49-
uses: actions/configure-pages@v3
49+
uses: actions/configure-pages@v4
5050

5151
- name: Install dependencies
5252
run: opam install . --deps-only --locked --with-doc
@@ -68,4 +68,4 @@ jobs:
6868
steps:
6969
- name: Deploy to GitHub Pages
7070
id: deployment
71-
uses: actions/deploy-pages@v2
71+
uses: actions/deploy-pages@v3

‎.github/workflows/locked.yml

+2-2
Original file line numberDiff line numberDiff line change
@@ -82,10 +82,10 @@ jobs:
8282
- name: Test incremental regression with cfg comparison
8383
run: ruby scripts/update_suite.rb -c
8484

85-
- uses: actions/upload-artifact@v3
85+
- uses: actions/upload-artifact@v4
8686
if: always()
8787
with:
88-
name: suite_result
88+
name: suite_result-${{ matrix.os }}
8989
path: tests/suite_result/
9090

9191
extraction:

‎.github/workflows/metadata.yml

+3
Original file line numberDiff line numberDiff line change
@@ -27,6 +27,9 @@ jobs:
2727
args: --validate
2828

2929
zenodo-validate:
30+
# Zenodo schema URL is dead
31+
if: ${{ false }}
32+
3033
strategy:
3134
matrix:
3235
node-version:

‎.github/workflows/options.yml

+3-3
Original file line numberDiff line numberDiff line change
@@ -26,10 +26,10 @@ jobs:
2626
run: npm install -g ajv-cli
2727

2828
- name: Migrate schema # https://github.com/ajv-validator/ajv-cli/issues/199
29-
run: ajv migrate -s src/common/util/options.schema.json
29+
run: ajv migrate -s src/config/options.schema.json
3030

3131
- name: Validate conf
32-
run: ajv validate -s src/common/util/options.schema.json -d "conf/**/*.json"
32+
run: ajv validate -s src/config/options.schema.json -d "conf/**/*.json"
3333

3434
- name: Validate incremental tests
35-
run: ajv validate -s src/common/util/options.schema.json -d "tests/incremental/*/*.json"
35+
run: ajv validate -s src/config/options.schema.json -d "tests/incremental/*/*.json"

‎.github/workflows/semgrep.yml

+1-1
Original file line numberDiff line numberDiff line change
@@ -22,7 +22,7 @@ jobs:
2222
run: semgrep scan --config .semgrep/ --sarif > semgrep.sarif
2323

2424
- name: Upload SARIF file to GitHub Advanced Security Dashboard
25-
uses: github/codeql-action/upload-sarif@v2
25+
uses: github/codeql-action/upload-sarif@v3
2626
with:
2727
sarif_file: semgrep.sarif
2828
if: always()

‎.gitignore

-1
Original file line numberDiff line numberDiff line change
@@ -29,7 +29,6 @@ linux-headers
2929
.goblint*/
3030
goblint_temp_*/
3131

32-
src/spec/graph
3332
.vagrant
3433

3534
g2html.jar

‎.mailmap

+4
Original file line numberDiff line numberDiff line change
@@ -23,6 +23,7 @@ Kerem Çakırer <[email protected]> <[email protected]>
2323
Sarah Tilscher <[email protected]>
2424
Karoliine Holter <[email protected]>
2525
<[email protected]> <[email protected]>
26+
<[email protected]> <[email protected]>
2627

2728
Elias Brandstetter <[email protected]> <[email protected]>
2829
wherekonshade <[email protected]> <[email protected]>
@@ -37,3 +38,6 @@ Mireia Cano Pujol <[email protected]>
3738
Felix Krayer <[email protected]>
3839
Felix Krayer <[email protected]> <[email protected]>
3940
Manuel Pietsch <[email protected]>
41+
Tim Ortel <[email protected]>
42+
Tomáš Dacík <[email protected]>
43+
<[email protected]> <[email protected]>

‎.readthedocs.yaml

+1-1
Original file line numberDiff line numberDiff line change
@@ -20,4 +20,4 @@ build:
2020
- pip install json-schema-for-humans
2121
post_build:
2222
- mkdir _readthedocs/html/jsfh/
23-
- generate-schema-doc --config-file jsfh.yml src/common/util/options.schema.json _readthedocs/html/jsfh/
23+
- generate-schema-doc --config-file jsfh.yml src/config/options.schema.json _readthedocs/html/jsfh/

‎.zenodo.json

+10-5
Original file line numberDiff line numberDiff line change
@@ -10,15 +10,18 @@
1010
},
1111
{
1212
"name": "Schwarz, Michael",
13-
"affiliation": "Technische Universität München"
13+
"affiliation": "Technische Universität München",
14+
"orcid": "0000-0002-9828-0308"
1415
},
1516
{
1617
"name": "Erhard, Julian",
17-
"affiliation": "Technische Universität München"
18+
"affiliation": "Technische Universität München",
19+
"orcid": "0000-0002-1729-3925"
1820
},
1921
{
2022
"name": "Tilscher, Sarah",
21-
"affiliation": "Technische Universität München"
23+
"affiliation": "Technische Universität München",
24+
"orcid": "0009-0009-9644-7475"
2225
},
2326
{
2427
"name": "Vogler, Ralf",
@@ -30,14 +33,16 @@
3033
},
3134
{
3235
"name": "Vojdani, Vesal",
33-
"affiliation": "University of Tartu"
36+
"affiliation": "University of Tartu",
37+
"orcid": "0000-0003-4336-7980"
3438
}
3539
],
3640
"contributors": [
3741
{
3842
"name": "Seidl, Helmut",
3943
"type": "ProjectLeader",
40-
"affiliation": "Technische Universität München"
44+
"affiliation": "Technische Universität München",
45+
"orcid": "0000-0002-2135-1593"
4146
},
4247
{
4348
"name": "Schwarz, Martin D.",

‎CHANGELOG.md

+12
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,15 @@
1+
## v2.3.0
2+
Functionally equivalent to Goblint in SV-COMP 2024.
3+
4+
* Add termination analysis for loops (#1093).
5+
* Add memory out-of-bounds analysis (#1094, #1197).
6+
* Add memory leak analysis (#1127, #1241, #1246).
7+
* Add SV-COMP `termination`, `valid-memsafety` and `valid-memcleanup` properties support (#1220, #1228, #1201, #1199, #1259, #1262).
8+
* Add YAML witness version 2.0 support (#1238, #1240, #1217, #1226, #1225, #1248).
9+
* Add final warnings about unsound results (#1190, #1191).
10+
* Add many library function specifications (#1167, #1174, #1203, #1205, #1212, #1220, #1239, #1242, #1244, #1254, #1269).
11+
* Adapt automatic configuration tuning (#912, #921, #987, #1168, #1214, #1234).
12+
113
## v2.2.1
214
* Bump batteries lower bound to 3.5.0.
315
* Fix flaky dead code elimination transformation test.

‎CITATION.cff

+4
Original file line numberDiff line numberDiff line change
@@ -12,12 +12,15 @@ authors: # same authors as in .zenodo.json and dune-project
1212
- given-names: Michael
1313
family-names: Schwarz
1414
affiliation: "Technische Universität München"
15+
orcid: "https://orcid.org/0000-0002-9828-0308"
1516
- given-names: Julian
1617
family-names: Erhard
1718
affiliation: "Technische Universität München"
19+
orcid: "https://orcid.org/0000-0002-1729-3925"
1820
- given-names: Sarah
1921
family-names: Tilscher
2022
affiliation: "Technische Universität München"
23+
orcid: "https://orcid.org/0009-0009-9644-7475"
2124
- given-names: Ralf
2225
family-names: Vogler
2326
affiliation: "Technische Universität München"
@@ -27,6 +30,7 @@ authors: # same authors as in .zenodo.json and dune-project
2730
- given-names: Vesal
2831
family-names: Vojdani
2932
affiliation: "University of Tartu"
33+
orcid: "https://orcid.org/0000-0003-4336-7980"
3034

3135
license: MIT
3236
repository-code: "https://github.com/goblint/analyzer"

‎conf/examples/very-precise.json

+3-1
Original file line numberDiff line numberDiff line change
@@ -61,7 +61,9 @@
6161
"structs" : {
6262
"domain" : "combined-sk"
6363
},
64-
"limit-string-addresses": false
64+
"strings": {
65+
"domain": "disjoint"
66+
}
6567
}
6668
},
6769
"exp": {

‎conf/ldv-races.json

+16-1
Original file line numberDiff line numberDiff line change
@@ -29,7 +29,9 @@
2929
"escape",
3030
"expRelation",
3131
"mhp",
32-
"assert"
32+
"assert",
33+
"var_eq",
34+
"symb_locks"
3335
],
3436
"malloc": {
3537
"wrappers": [
@@ -52,6 +54,19 @@
5254
]
5355
}
5456
},
57+
"lib": {
58+
"activated": [
59+
"c",
60+
"posix",
61+
"pthread",
62+
"gcc",
63+
"glibc",
64+
"linux-userspace",
65+
"goblint",
66+
"ncurses",
67+
"klever"
68+
]
69+
},
5570
"witness": {
5671
"graphml": {
5772
"enabled": true,

‎conf/min-unsound.json

+6
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
{
2+
"ana": {
3+
"activated": [
4+
]
5+
}
6+
}

‎conf/svcomp.json

+44-3
Original file line numberDiff line numberDiff line change
@@ -32,6 +32,15 @@
3232
"thread",
3333
"threadJoins"
3434
],
35+
"path_sens": [
36+
"mutex",
37+
"malloc_null",
38+
"uninit",
39+
"expsplit",
40+
"activeSetjmp",
41+
"memLeak",
42+
"threadflag"
43+
],
3544
"context": {
3645
"widen": false
3746
},
@@ -52,14 +61,19 @@
5261

5362
"ldv_xmalloc",
5463
"ldv_xzalloc",
55-
"ldv_calloc"
64+
"ldv_calloc",
65+
"ldv_kzalloc"
5666
]
5767
},
5868
"base": {
5969
"arrays": {
6070
"domain": "partitioned"
6171
}
6272
},
73+
"race": {
74+
"free": false,
75+
"call": false
76+
},
6377
"autotune": {
6478
"enabled": true,
6579
"activated": [
@@ -72,8 +86,8 @@
7286
"wideningThresholds",
7387
"loopUnrollHeuristic",
7488
"memsafetySpecification",
75-
"tmpSpecialAnalysis",
76-
"termination"
89+
"termination",
90+
"tmpSpecialAnalysis"
7791
]
7892
}
7993
},
@@ -97,6 +111,33 @@
97111
"enabled": true,
98112
"id": "enumerate",
99113
"unknown": false
114+
},
115+
"yaml": {
116+
"enabled": true,
117+
"format-version": "2.0",
118+
"entry-types": [
119+
"invariant_set"
120+
],
121+
"invariant-types": [
122+
"loop_invariant"
123+
]
124+
},
125+
"invariant": {
126+
"loop-head": true,
127+
"after-lock": false,
128+
"other": false,
129+
"accessed": false,
130+
"exact": true,
131+
"exclude-vars": [
132+
"tmp\\(___[0-9]+\\)?",
133+
"cond",
134+
"RETURN",
135+
"__\\(cil_\\)?tmp_?[0-9]*\\(_[0-9]+\\)?",
136+
".*____CPAchecker_TMP_[0-9]+",
137+
"__VERIFIER_assert__cond",
138+
"__ksymtab_.*",
139+
"\\(ldv_state_variable\\|ldv_timer_state\\|ldv_timer_list\\|ldv_irq_\\(line_\\|data_\\)?[0-9]+\\|ldv_retval\\)_[0-9]+"
140+
]
100141
}
101142
},
102143
"pre": {

0 commit comments

Comments
 (0)