Skip to content

Commit 2b61d84

Browse files
sim642sim642
authored
Merge pull request #1845 from goblint/multishot-svcomp25
Executing a Portfolio of Runs via Script
2 parents 44fc62a + 0568afb commit 2b61d84

File tree

7 files changed

+717
-0
lines changed

7 files changed

+717
-0
lines changed

‎conf/svcomp26/level00.json‎

Lines changed: 108 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,108 @@
1+
{
2+
"ana": {
3+
"sv-comp": {
4+
"enabled": true,
5+
"functions": true
6+
},
7+
"int": {
8+
"def_exc": true,
9+
"enums": false
10+
},
11+
"float": {
12+
"interval": false,
13+
"evaluate_math_functions": false
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+
"symb_locks",
30+
"region",
31+
"thread",
32+
"threadJoins",
33+
"abortUnless"
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+
"base": {
48+
"arrays": {
49+
"domain": "partitioned"
50+
}
51+
},
52+
"race": {
53+
"free": false,
54+
"call": false
55+
},
56+
"autotune": {
57+
"enabled": true,
58+
"activated": [
59+
"reduceAnalyses",
60+
"mallocWrappers",
61+
"noRecursiveIntervals",
62+
"wideningThresholds",
63+
"loopUnrollHeuristic",
64+
"memsafetySpecification",
65+
"noOverflows",
66+
"termination",
67+
"tmpSpecialAnalysis"
68+
]
69+
}
70+
},
71+
"exp": {
72+
"region-offsets": true
73+
},
74+
"solver": "td3",
75+
"sem": {
76+
"unknown_function": {
77+
"spawn": false
78+
},
79+
"int": {
80+
"signed_overflow": "assume_none"
81+
},
82+
"null-pointer": {
83+
"dereference": "assume_none"
84+
}
85+
},
86+
"witness": {
87+
"yaml": {
88+
"enabled": true,
89+
"format-version": "2.0",
90+
"entry-types": [
91+
"invariant_set"
92+
],
93+
"invariant-types": [
94+
"loop_invariant"
95+
]
96+
},
97+
"invariant": {
98+
"loop-head": true,
99+
"after-lock": false,
100+
"other": false,
101+
"accessed": false,
102+
"exact": true
103+
}
104+
},
105+
"pre": {
106+
"enabled": false
107+
}
108+
}

‎conf/svcomp26/level01.json‎

Lines changed: 114 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,114 @@
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+
"reduceAnalyses",
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+
"yaml": {
93+
"enabled": true,
94+
"sv-comp-true-only": false,
95+
"format-version": "2.0",
96+
"entry-types": [
97+
"invariant_set"
98+
],
99+
"invariant-types": [
100+
"loop_invariant"
101+
]
102+
},
103+
"invariant": {
104+
"loop-head": true,
105+
"after-lock": false,
106+
"other": false,
107+
"accessed": false,
108+
"exact": true
109+
}
110+
},
111+
"pre": {
112+
"enabled": false
113+
}
114+
}

‎conf/svcomp26/level02.json‎

Lines changed: 129 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,129 @@
1+
{
2+
"ana": {
3+
"sv-comp": {
4+
"enabled": true,
5+
"functions": true
6+
},
7+
"int": {
8+
"def_exc": true,
9+
"enums": true,
10+
"congruence": true,
11+
"bitfield":true,
12+
"interval": true
13+
},
14+
"float": {
15+
"interval": true,
16+
"evaluate_math_functions": true
17+
},
18+
"activated": [
19+
"base",
20+
"threadid",
21+
"threadflag",
22+
"threadreturn",
23+
"mallocWrapper",
24+
"mutexEvents",
25+
"mutex",
26+
"access",
27+
"race",
28+
"escape",
29+
"expRelation",
30+
"mhp",
31+
"assert",
32+
"var_eq",
33+
"symb_locks",
34+
"region",
35+
"thread",
36+
"threadJoins",
37+
"abortUnless",
38+
"affeq",
39+
"apron"
40+
],
41+
"apron": {
42+
"domain": "octagon"
43+
},
44+
"path_sens": [
45+
"mutex",
46+
"malloc_null",
47+
"uninit",
48+
"expsplit",
49+
"activeSetjmp",
50+
"memLeak",
51+
"threadflag"
52+
],
53+
"context": {
54+
"widen": false
55+
},
56+
"base": {
57+
"arrays": {
58+
"domain": "partitioned"
59+
},
60+
"structs": {
61+
"domain": "sets"
62+
}
63+
},
64+
"race": {
65+
"free": false,
66+
"call": false
67+
},
68+
"autotune": {
69+
"enabled": true,
70+
"activated": [
71+
"reduceAnalyses",
72+
"mallocWrappers",
73+
"noRecursiveIntervals",
74+
"enums",
75+
"congruence",
76+
"octagon",
77+
"wideningThresholds",
78+
"loopUnrollHeuristic",
79+
"memsafetySpecification",
80+
"noOverflows",
81+
"termination",
82+
"tmpSpecialAnalysis"
83+
]
84+
}
85+
},
86+
"exp": {
87+
"region-offsets": true
88+
},
89+
"solver": "td3",
90+
"solvers": {
91+
"td3": {
92+
"widen_gas": 30,
93+
"side_widen_gas": 30
94+
}
95+
},
96+
"sem": {
97+
"unknown_function": {
98+
"spawn": false
99+
},
100+
"int": {
101+
"signed_overflow": "assume_none"
102+
},
103+
"null-pointer": {
104+
"dereference": "assume_none"
105+
}
106+
},
107+
"witness": {
108+
"yaml": {
109+
"enabled": true,
110+
"format-version": "2.0",
111+
"entry-types": [
112+
"invariant_set"
113+
],
114+
"invariant-types": [
115+
"loop_invariant"
116+
]
117+
},
118+
"invariant": {
119+
"loop-head": true,
120+
"after-lock": false,
121+
"other": false,
122+
"accessed": false,
123+
"exact": true
124+
}
125+
},
126+
"pre": {
127+
"enabled": false
128+
}
129+
}

0 commit comments

Comments
 (0)