Skip to content

Commit 315c8b7

Browse files
sim642sim642
authored
Merge pull request #1841 from goblint/svcomp26-dev
SV-COMP 2026 development
2 parents 526af75 + bb55b70 commit 315c8b7

35 files changed

+552
-567
lines changed

‎.gitignore‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -54,6 +54,7 @@ goblint.bc.js
5454
*.rej
5555

5656
sv-comp/goblint.zip
57+
scripts/sv-comp/goblint.zip
5758

5859
privPrecCompare
5960
privPrecCompare-creduce

‎Makefile‎

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2,3 +2,21 @@ native :
22

33
% :
44
@./make.sh $@
5+
6+
7+
.PHONY: sv-comp-tag sv-comp-build sv-comp-smoketest-ubuntu sv-comp-smoketest-competition sv-comp-smoketest sv-comp
8+
9+
sv-comp-tag:
10+
git tag -m "SV-COMP 2026" svcomp26
11+
12+
sv-comp-build: sv-comp-tag
13+
docker build . -f scripts/sv-comp/Dockerfile --output=scripts/sv-comp/
14+
15+
sv-comp-smoketest-ubuntu: sv-comp-tag
16+
docker build . -f scripts/sv-comp/Dockerfile --target smoketest-ubuntu
17+
18+
sv-comp-smoketest-competition: sv-comp-tag
19+
docker build . -f scripts/sv-comp/Dockerfile --target smoketest-competition
20+
21+
sv-comp-smoketest: sv-comp-smoketest-ubuntu sv-comp-smoketest-competition;
22+
sv-comp: sv-comp-smoketest sv-comp-build;

‎conf/svcomp-validate.json‎

Lines changed: 0 additions & 118 deletions
This file was deleted.

‎conf/svcomp26/common.json‎

Lines changed: 52 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,52 @@
1+
{
2+
"ana": {
3+
"sv-comp": {
4+
"enabled": true,
5+
"functions": true
6+
},
7+
"int": {
8+
"def_exc": true
9+
},
10+
"context": {
11+
"widen": false
12+
},
13+
"race": {
14+
"free": false,
15+
"call": false
16+
},
17+
"autotune": {
18+
"enabled": true
19+
}
20+
},
21+
"exp": {
22+
"region-offsets": true
23+
},
24+
"solver": "td3",
25+
"solvers": {
26+
"td3": {
27+
"weak-deps": "lazy"
28+
}
29+
},
30+
"sem": {
31+
"unknown_function": {
32+
"spawn": false
33+
},
34+
"int": {
35+
"signed_overflow": "assume_none"
36+
},
37+
"null-pointer": {
38+
"dereference": "assume_none"
39+
}
40+
},
41+
"witness": {
42+
"yaml": {
43+
"format-version": "2.1"
44+
},
45+
"invariant": {
46+
"loop-head": true
47+
}
48+
},
49+
"pre": {
50+
"transform-paths": false
51+
}
52+
}

‎conf/svcomp26/level00.json‎

Lines changed: 5 additions & 51 deletions
Original file line numberDiff line numberDiff line change
@@ -1,12 +1,7 @@
11
{
22
"ana": {
3-
"sv-comp": {
4-
"enabled": true,
5-
"functions": true
6-
},
73
"int": {
8-
"def_exc": true,
9-
"enums": false
4+
"enums": false
105
},
116
"float": {
127
"interval": false,
@@ -30,7 +25,9 @@
3025
"region",
3126
"thread",
3227
"threadJoins",
33-
"abortUnless"
28+
"abortUnless",
29+
"mutexGhosts",
30+
"pthreadMutexType"
3431
],
3532
"path_sens": [
3633
"mutex",
@@ -39,23 +36,17 @@
3936
"expsplit",
4037
"activeSetjmp",
4138
"memLeak",
42-
"threadflag"
39+
"threadflag"
4340
],
4441
"context": {
45-
"widen": false,
4642
"gas_value": 30
4743
},
4844
"base": {
4945
"arrays": {
5046
"domain": "partitioned"
5147
}
5248
},
53-
"race": {
54-
"free": false,
55-
"call": false
56-
},
5749
"autotune": {
58-
"enabled": true,
5950
"activated": [
6051
"reduceAnalyses",
6152
"mallocWrappers",
@@ -68,42 +59,5 @@
6859
"tmpSpecialAnalysis"
6960
]
7061
}
71-
},
72-
"exp": {
73-
"region-offsets": true
74-
},
75-
"solver": "td3",
76-
"sem": {
77-
"unknown_function": {
78-
"spawn": false
79-
},
80-
"int": {
81-
"signed_overflow": "assume_none"
82-
},
83-
"null-pointer": {
84-
"dereference": "assume_none"
85-
}
86-
},
87-
"witness": {
88-
"yaml": {
89-
"enabled": true,
90-
"format-version": "2.0",
91-
"entry-types": [
92-
"invariant_set"
93-
],
94-
"invariant-types": [
95-
"loop_invariant"
96-
]
97-
},
98-
"invariant": {
99-
"loop-head": true,
100-
"after-lock": false,
101-
"other": false,
102-
"accessed": false,
103-
"exact": true
104-
}
105-
},
106-
"pre": {
107-
"enabled": false
10862
}
10963
}

‎conf/svcomp26/level01.json‎

Lines changed: 3 additions & 50 deletions
Original file line numberDiff line numberDiff line change
@@ -1,11 +1,6 @@
11
{
22
"ana": {
3-
"sv-comp": {
4-
"enabled": true,
5-
"functions": true
6-
},
73
"int": {
8-
"def_exc": true,
94
"enums": false,
105
"interval": true
116
},
@@ -32,7 +27,9 @@
3227
"region",
3328
"thread",
3429
"threadJoins",
35-
"abortUnless"
30+
"abortUnless",
31+
"mutexGhosts",
32+
"pthreadMutexType"
3633
],
3734
"path_sens": [
3835
"mutex",
@@ -44,20 +41,14 @@
4441
"threadflag"
4542
],
4643
"context": {
47-
"widen": false,
4844
"gas_value": 30
4945
},
5046
"base": {
5147
"arrays": {
5248
"domain": "partitioned"
5349
}
5450
},
55-
"race": {
56-
"free": false,
57-
"call": false
58-
},
5951
"autotune": {
60-
"enabled": true,
6152
"activated": [
6253
"reduceAnalyses",
6354
"mallocWrappers",
@@ -73,43 +64,5 @@
7364
"tmpSpecialAnalysis"
7465
]
7566
}
76-
},
77-
"exp": {
78-
"region-offsets": true
79-
},
80-
"solver": "td3",
81-
"sem": {
82-
"unknown_function": {
83-
"spawn": false
84-
},
85-
"int": {
86-
"signed_overflow": "assume_none"
87-
},
88-
"null-pointer": {
89-
"dereference": "assume_none"
90-
}
91-
},
92-
"witness": {
93-
"yaml": {
94-
"enabled": true,
95-
"sv-comp-true-only": false,
96-
"format-version": "2.0",
97-
"entry-types": [
98-
"invariant_set"
99-
],
100-
"invariant-types": [
101-
"loop_invariant"
102-
]
103-
},
104-
"invariant": {
105-
"loop-head": true,
106-
"after-lock": false,
107-
"other": false,
108-
"accessed": false,
109-
"exact": true
110-
}
111-
},
112-
"pre": {
113-
"enabled": false
11467
}
11568
}

0 commit comments

Comments
 (0)