Skip to content

Commit cd2428a

Browse files
sim642sim642
authored
Merge pull request #1257 from goblint/svcomp24-dev
SV-COMP 2024 development
2 parents 3540ae2 + c2e9465 commit cd2428a

36 files changed

+1212
-89
lines changed

‎CHANGELOG.md‎

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,15 @@
1+
## v2.3.0 (unreleased)
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.

‎conf/svcomp.json‎

Lines changed: 44 additions & 3 deletions
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": {

‎conf/svcomp24-validate.json‎

Lines changed: 140 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,140 @@
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+
},
15+
"activated": [
16+
"base",
17+
"threadid",
18+
"threadflag",
19+
"threadreturn",
20+
"mallocWrapper",
21+
"mutexEvents",
22+
"mutex",
23+
"access",
24+
"race",
25+
"escape",
26+
"expRelation",
27+
"mhp",
28+
"assert",
29+
"var_eq",
30+
"symb_locks",
31+
"region",
32+
"thread",
33+
"threadJoins",
34+
"unassume"
35+
],
36+
"path_sens": [
37+
"mutex",
38+
"malloc_null",
39+
"uninit",
40+
"expsplit",
41+
"activeSetjmp",
42+
"memLeak",
43+
"threadflag"
44+
],
45+
"context": {
46+
"widen": false
47+
},
48+
"malloc": {
49+
"wrappers": [
50+
"kmalloc",
51+
"__kmalloc",
52+
"usb_alloc_urb",
53+
"__builtin_alloca",
54+
"kzalloc",
55+
56+
"ldv_malloc",
57+
58+
"kzalloc_node",
59+
"ldv_zalloc",
60+
"kmalloc_array",
61+
"kcalloc",
62+
63+
"ldv_xmalloc",
64+
"ldv_xzalloc",
65+
"ldv_calloc",
66+
"ldv_kzalloc"
67+
]
68+
},
69+
"base": {
70+
"arrays": {
71+
"domain": "partitioned"
72+
}
73+
},
74+
"race": {
75+
"free": false,
76+
"call": false
77+
},
78+
"autotune": {
79+
"enabled": true,
80+
"activated": [
81+
"singleThreaded",
82+
"mallocWrappers",
83+
"noRecursiveIntervals",
84+
"enums",
85+
"congruence",
86+
"octagon",
87+
"wideningThresholds",
88+
"loopUnrollHeuristic",
89+
"memsafetySpecification",
90+
"termination",
91+
"tmpSpecialAnalysis"
92+
]
93+
},
94+
"widen": {
95+
"tokens": true
96+
}
97+
},
98+
"exp": {
99+
"region-offsets": true
100+
},
101+
"solver": "td3",
102+
"sem": {
103+
"unknown_function": {
104+
"spawn": false
105+
},
106+
"int": {
107+
"signed_overflow": "assume_none"
108+
},
109+
"null-pointer": {
110+
"dereference": "assume_none"
111+
}
112+
},
113+
"witness": {
114+
"graphml": {
115+
"enabled": false
116+
},
117+
"yaml": {
118+
"enabled": false,
119+
"strict": true,
120+
"format-version": "2.0",
121+
"entry-types": [
122+
"location_invariant",
123+
"loop_invariant",
124+
"invariant_set"
125+
],
126+
"invariant-types": [
127+
"location_invariant",
128+
"loop_invariant"
129+
]
130+
},
131+
"invariant": {
132+
"loop-head": true,
133+
"after-lock": true,
134+
"other": true
135+
}
136+
},
137+
"pre": {
138+
"enabled": false
139+
}
140+
}

‎conf/svcomp24.json‎

Lines changed: 146 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,146 @@
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+
},
15+
"activated": [
16+
"base",
17+
"threadid",
18+
"threadflag",
19+
"threadreturn",
20+
"mallocWrapper",
21+
"mutexEvents",
22+
"mutex",
23+
"access",
24+
"race",
25+
"escape",
26+
"expRelation",
27+
"mhp",
28+
"assert",
29+
"var_eq",
30+
"symb_locks",
31+
"region",
32+
"thread",
33+
"threadJoins"
34+
],
35+
"path_sens": [
36+
"mutex",
37+
"malloc_null",
38+
"uninit",
39+
"expsplit",
40+
"activeSetjmp",
41+
"memLeak",
42+
"threadflag"
43+
],
44+
"context": {
45+
"widen": false
46+
},
47+
"malloc": {
48+
"wrappers": [
49+
"kmalloc",
50+
"__kmalloc",
51+
"usb_alloc_urb",
52+
"__builtin_alloca",
53+
"kzalloc",
54+
55+
"ldv_malloc",
56+
57+
"kzalloc_node",
58+
"ldv_zalloc",
59+
"kmalloc_array",
60+
"kcalloc",
61+
62+
"ldv_xmalloc",
63+
"ldv_xzalloc",
64+
"ldv_calloc",
65+
"ldv_kzalloc"
66+
]
67+
},
68+
"base": {
69+
"arrays": {
70+
"domain": "partitioned"
71+
}
72+
},
73+
"race": {
74+
"free": false,
75+
"call": false
76+
},
77+
"autotune": {
78+
"enabled": true,
79+
"activated": [
80+
"singleThreaded",
81+
"mallocWrappers",
82+
"noRecursiveIntervals",
83+
"enums",
84+
"congruence",
85+
"octagon",
86+
"wideningThresholds",
87+
"loopUnrollHeuristic",
88+
"memsafetySpecification",
89+
"termination",
90+
"tmpSpecialAnalysis"
91+
]
92+
}
93+
},
94+
"exp": {
95+
"region-offsets": true
96+
},
97+
"solver": "td3",
98+
"sem": {
99+
"unknown_function": {
100+
"spawn": false
101+
},
102+
"int": {
103+
"signed_overflow": "assume_none"
104+
},
105+
"null-pointer": {
106+
"dereference": "assume_none"
107+
}
108+
},
109+
"witness": {
110+
"graphml": {
111+
"enabled": true,
112+
"id": "enumerate",
113+
"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+
]
141+
}
142+
},
143+
"pre": {
144+
"enabled": false
145+
}
146+
}

0 commit comments

Comments
 (0)