Skip to content

Commit 3c75f15

Browse files
sim642sim642
committed
Merge branch 'master' into yaml-witness-ghost
2 parents 2c25848 + 68cd952 commit 3c75f15

59 files changed

Lines changed: 678 additions & 134 deletions

Some content is hidden

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

‎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: 4 additions & 33 deletions
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,8 @@
1010
"interval": true
1111
},
1212
"float": {
13-
"interval": true
13+
"interval": true,
14+
"evaluate_math_functions": true
1415
},
1516
"activated": [
1617
"base",
@@ -47,27 +48,6 @@
4748
"context": {
4849
"widen": false
4950
},
50-
"malloc": {
51-
"wrappers": [
52-
"kmalloc",
53-
"__kmalloc",
54-
"usb_alloc_urb",
55-
"__builtin_alloca",
56-
"kzalloc",
57-
58-
"ldv_malloc",
59-
60-
"kzalloc_node",
61-
"ldv_zalloc",
62-
"kmalloc_array",
63-
"kcalloc",
64-
65-
"ldv_xmalloc",
66-
"ldv_xzalloc",
67-
"ldv_calloc",
68-
"ldv_kzalloc"
69-
]
70-
},
7151
"base": {
7252
"arrays": {
7353
"domain": "partitioned"
@@ -110,6 +90,7 @@
11090
"wideningThresholds",
11191
"loopUnrollHeuristic",
11292
"memsafetySpecification",
93+
"noOverflows",
11394
"termination",
11495
"tmpSpecialAnalysis"
11596
]
@@ -149,17 +130,7 @@
149130
"accessed": false,
150131
"exact": true,
151132
"all-locals": false,
152-
"flow_insensitive-as": "invariant_set-location_invariant",
153-
"exclude-vars": [
154-
"tmp\\(___[0-9]+\\)?",
155-
"cond",
156-
"RETURN",
157-
"__\\(cil_\\)?tmp_?[0-9]*\\(_[0-9]+\\)?",
158-
".*____CPAchecker_TMP_[0-9]+",
159-
"__VERIFIER_assert__cond",
160-
"__ksymtab_.*",
161-
"\\(ldv_state_variable\\|ldv_timer_state\\|ldv_timer_list\\|ldv_irq_\\(line_\\|data_\\)?[0-9]+\\|ldv_retval\\)_[0-9]+"
162-
]
133+
"flow_insensitive-as": "invariant_set-location_invariant"
163134
}
164135
},
165136
"pre": {

‎conf/svcomp-validate.json‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,8 @@
1010
"interval": true
1111
},
1212
"float": {
13-
"interval": true
13+
"interval": true,
14+
"evaluate_math_functions": true
1415
},
1516
"activated": [
1617
"base",

‎conf/svcomp.json‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,8 @@
1010
"interval": true
1111
},
1212
"float": {
13-
"interval": true
13+
"interval": true,
14+
"evaluate_math_functions": true
1415
},
1516
"activated": [
1617
"base",

‎conf/svcomp24-validate.json‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,8 @@
1010
"interval": true
1111
},
1212
"float": {
13-
"interval": true
13+
"interval": true,
14+
"evaluate_math_functions": true
1415
},
1516
"activated": [
1617
"base",

‎conf/svcomp24.json‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,8 @@
1010
"interval": true
1111
},
1212
"float": {
13-
"interval": true
13+
"interval": true,
14+
"evaluate_math_functions": true
1415
},
1516
"activated": [
1617
"base",

‎conf/svcomp25-validate.json‎

Lines changed: 123 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,123 @@
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+
"unassume"
37+
],
38+
"path_sens": [
39+
"mutex",
40+
"malloc_null",
41+
"uninit",
42+
"expsplit",
43+
"activeSetjmp",
44+
"memLeak",
45+
"threadflag"
46+
],
47+
"context": {
48+
"widen": false
49+
},
50+
"base": {
51+
"arrays": {
52+
"domain": "partitioned"
53+
}
54+
},
55+
"race": {
56+
"free": false,
57+
"call": false
58+
},
59+
"autotune": {
60+
"enabled": true,
61+
"activated": [
62+
"singleThreaded",
63+
"mallocWrappers",
64+
"noRecursiveIntervals",
65+
"enums",
66+
"congruence",
67+
"octagon",
68+
"wideningThresholds",
69+
"loopUnrollHeuristic",
70+
"memsafetySpecification",
71+
"noOverflows",
72+
"termination",
73+
"tmpSpecialAnalysis"
74+
]
75+
},
76+
"widen": {
77+
"tokens": true
78+
}
79+
},
80+
"exp": {
81+
"region-offsets": true
82+
},
83+
"solver": "td3",
84+
"sem": {
85+
"unknown_function": {
86+
"spawn": false
87+
},
88+
"int": {
89+
"signed_overflow": "assume_none"
90+
},
91+
"null-pointer": {
92+
"dereference": "assume_none"
93+
}
94+
},
95+
"witness": {
96+
"graphml": {
97+
"enabled": false
98+
},
99+
"yaml": {
100+
"enabled": false,
101+
"strict": true,
102+
"format-version": "2.0",
103+
"entry-types": [
104+
"location_invariant",
105+
"loop_invariant",
106+
"invariant_set",
107+
"violation_sequence"
108+
],
109+
"invariant-types": [
110+
"location_invariant",
111+
"loop_invariant"
112+
]
113+
},
114+
"invariant": {
115+
"loop-head": true,
116+
"after-lock": true,
117+
"other": true
118+
}
119+
},
120+
"pre": {
121+
"enabled": false
122+
}
123+
}

‎conf/svcomp25.json‎

Lines changed: 118 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,118 @@
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+
],
37+
"path_sens": [
38+
"mutex",
39+
"malloc_null",
40+
"uninit",
41+
"expsplit",
42+
"activeSetjmp",
43+
"memLeak",
44+
"threadflag"
45+
],
46+
"context": {
47+
"widen": false
48+
},
49+
"base": {
50+
"arrays": {
51+
"domain": "partitioned"
52+
}
53+
},
54+
"race": {
55+
"free": false,
56+
"call": false
57+
},
58+
"autotune": {
59+
"enabled": true,
60+
"activated": [
61+
"singleThreaded",
62+
"mallocWrappers",
63+
"noRecursiveIntervals",
64+
"enums",
65+
"congruence",
66+
"octagon",
67+
"wideningThresholds",
68+
"loopUnrollHeuristic",
69+
"memsafetySpecification",
70+
"noOverflows",
71+
"termination",
72+
"tmpSpecialAnalysis"
73+
]
74+
}
75+
},
76+
"exp": {
77+
"region-offsets": true
78+
},
79+
"solver": "td3",
80+
"sem": {
81+
"unknown_function": {
82+
"spawn": false
83+
},
84+
"int": {
85+
"signed_overflow": "assume_none"
86+
},
87+
"null-pointer": {
88+
"dereference": "assume_none"
89+
}
90+
},
91+
"witness": {
92+
"graphml": {
93+
"enabled": true,
94+
"id": "enumerate",
95+
"unknown": false
96+
},
97+
"yaml": {
98+
"enabled": true,
99+
"format-version": "2.0",
100+
"entry-types": [
101+
"invariant_set"
102+
],
103+
"invariant-types": [
104+
"loop_invariant"
105+
]
106+
},
107+
"invariant": {
108+
"loop-head": true,
109+
"after-lock": false,
110+
"other": false,
111+
"accessed": false,
112+
"exact": true
113+
}
114+
},
115+
"pre": {
116+
"enabled": false
117+
}
118+
}

‎docs/developer-guide/releasing.md‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -77,6 +77,8 @@
7777

7878
This includes: git tag name, git tag message and zipped conf file.
7979

80+
5. Open MR with conf file name to the [bench-defs](https://gitlab.com/sosy-lab/sv-comp/bench-defs) repository.
81+
8082
### For each prerun
8183

8284
1. Update opam pins:

‎dune-project‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -16,7 +16,7 @@
1616
(homepage "https://goblint.in.tum.de")
1717
(documentation "https://goblint.readthedocs.io/en/latest/")
1818
(authors "Simmo Saan" "Michael Schwarz" "Julian Erhard" "Sarah Tilscher" "Karoliine Holter" "Ralf Vogler" "Kalmer Apinis" "Vesal Vojdani" ) ; same authors as in .zenodo.json and CITATION.cff
19-
(maintainers "Simmo Saan <simmo.saan@gmail.com>" "Michael Schwarz <michael.schwarz93@gmail.com>" "Karoliine Holter")
19+
(maintainers "Simmo Saan <simmo.saan@gmail.com>" "Michael Schwarz <michael.schwarz93@gmail.com>" "Karoliine Holter <karoliine.holter@ut.ee>")
2020
(license MIT)
2121

2222
(package
@@ -37,7 +37,7 @@ Goblint includes analyses for assertions, overflows, deadlocks, etc and can be e
3737
"concurrency"))
3838
(depends
3939
(ocaml (>= 4.14))
40-
(goblint-cil (>= 2.0.4)) ; TODO no way to define as pin-depends? Used goblint.opam.template to add it for now. https://github.com/ocaml/dune/issues/3231. Alternatively, removing this line and adding cil as a git submodule and `(vendored_dirs cil)` as ./dune also works. This way, no more need to reinstall the pinned cil opam package on changes. However, then cil is cleaned and has to be rebuild together with goblint.
40+
(goblint-cil (>= 2.0.5)) ; TODO no way to define as pin-depends? Used goblint.opam.template to add it for now. https://github.com/ocaml/dune/issues/3231. Alternatively, removing this line and adding cil as a git submodule and `(vendored_dirs cil)` as ./dune also works. This way, no more need to reinstall the pinned cil opam package on changes. However, then cil is cleaned and has to be rebuild together with goblint.
4141
(batteries (>= 3.5.1))
4242
(zarith (>= 1.10))
4343
(yojson (>= 2.0.0))

0 commit comments

Comments
 (0)