Skip to content

Commit 76e3b5d

Browse files
DrMichaelPetterDrMichaelPetter
committed
more detailed portfolio
1 parent f56f689 commit 76e3b5d

File tree

7 files changed

+418
-46
lines changed

7 files changed

+418
-46
lines changed

‎conf/svcomp26/level00.json‎

Lines changed: 5 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -6,12 +6,11 @@
66
},
77
"int": {
88
"def_exc": true,
9-
"enums": false,
10-
"interval": true
9+
"enums": false
1110
},
1211
"float": {
13-
"interval": true,
14-
"evaluate_math_functions": true
12+
"interval": false,
13+
"evaluate_math_functions": false
1514
},
1615
"activated": [
1716
"base",
@@ -27,12 +26,11 @@
2726
"expRelation",
2827
"mhp",
2928
"assert",
30-
"var_eq",
3129
"symb_locks",
3230
"region",
3331
"thread",
3432
"threadJoins",
35-
"abortUnless"
33+
"abortUnless"
3634
],
3735
"path_sens": [
3836
"mutex",
@@ -41,7 +39,7 @@
4139
"expsplit",
4240
"activeSetjmp",
4341
"memLeak",
44-
"threadflag"
42+
"threadflag"
4543
],
4644
"context": {
4745
"widen": false
@@ -61,9 +59,6 @@
6159
"reduceAnalyses",
6260
"mallocWrappers",
6361
"noRecursiveIntervals",
64-
"enums",
65-
"congruence",
66-
"octagon",
6762
"wideningThresholds",
6863
"loopUnrollHeuristic",
6964
"memsafetySpecification",

‎conf/svcomp26/level01.json‎

Lines changed: 9 additions & 27 deletions
Original file line numberDiff line numberDiff line change
@@ -6,11 +6,8 @@
66
},
77
"int": {
88
"def_exc": true,
9-
"enums": true,
10-
"congruence": true,
11-
"interval": true,
12-
"bitfield":true,
13-
"interval_threshold_widening": true
9+
"enums": false,
10+
"interval": true
1411
},
1512
"float": {
1613
"interval": true,
@@ -35,12 +32,8 @@
3532
"region",
3633
"thread",
3734
"threadJoins",
38-
"abortUnless",
39-
"apron"
35+
"abortUnless"
4036
],
41-
"apron":{
42-
"domain":"polyhedra"
43-
},
4437
"path_sens": [
4538
"mutex",
4639
"malloc_null",
@@ -51,18 +44,11 @@
5144
"threadflag"
5245
],
5346
"context": {
54-
"widen": false,
55-
"callString_length":3,
56-
"gas_scope": "function",
57-
"gas_value":60
47+
"widen": false
5848
},
5949
"base": {
6050
"arrays": {
61-
"domain": "unroll",
62-
"unrolling-factor": 128
63-
},
64-
"structs":{
65-
"domain": "sets"
51+
"domain": "partitioned"
6652
}
6753
},
6854
"race": {
@@ -77,7 +63,9 @@
7763
"noRecursiveIntervals",
7864
"enums",
7965
"congruence",
66+
"octagon",
8067
"wideningThresholds",
68+
"loopUnrollHeuristic",
8169
"memsafetySpecification",
8270
"noOverflows",
8371
"termination",
@@ -86,16 +74,9 @@
8674
}
8775
},
8876
"exp": {
89-
"region-offsets": true,
90-
"unrolling-factor": 128
77+
"region-offsets": true
9178
},
9279
"solver": "td3",
93-
"solvers":{
94-
"td3":{
95-
"side_widen_gas":60,
96-
"widen_gas":60
97-
}
98-
},
9980
"sem": {
10081
"unknown_function": {
10182
"spawn": false
@@ -110,6 +91,7 @@
11091
"witness": {
11192
"yaml": {
11293
"enabled": true,
94+
"sv-comp-true-only": false,
11395
"format-version": "2.0",
11496
"entry-types": [
11597
"invariant_set"

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

‎conf/svcomp26/level03.json‎

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

0 commit comments

Comments
 (0)