Skip to content

Commit ff77a63

Browse files
sim642sim642
committed
Merge branch 'master' into intdomain-split
2 parents db37e85 + 87ce3a5 commit ff77a63

File tree

136 files changed

+4300
-298
lines changed

Some content is hidden

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

136 files changed

+4300
-298
lines changed

‎.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+
}

‎conf/svcomp-validate.json‎

Lines changed: 3 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",
@@ -67,6 +68,7 @@
6768
"wideningThresholds",
6869
"loopUnrollHeuristic",
6970
"memsafetySpecification",
71+
"noOverflows",
7072
"termination",
7173
"tmpSpecialAnalysis"
7274
]

‎conf/svcomp.json‎

Lines changed: 3 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",
@@ -66,6 +67,7 @@
6667
"wideningThresholds",
6768
"loopUnrollHeuristic",
6869
"memsafetySpecification",
70+
"noOverflows",
6971
"termination",
7072
"tmpSpecialAnalysis"
7173
]

‎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+
}

0 commit comments

Comments
 (0)