Skip to content

Commit 73eb8ef

Browse files
DrMichaelPetterDrMichaelPetter
committed
first portfolio
1 parent d026615 commit 73eb8ef

File tree

3 files changed

+250
-0
lines changed

3 files changed

+250
-0
lines changed

‎conf/svcomp26/level00.json‎

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

‎conf/svcomp26/level01.json‎

Lines changed: 133 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,133 @@
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+
"interval": true,
12+
"bitfield":true,
13+
"interval_threshold_widening": true
14+
},
15+
"float": {
16+
"interval": true,
17+
"evaluate_math_functions": true
18+
},
19+
"activated": [
20+
"base",
21+
"threadid",
22+
"threadflag",
23+
"threadreturn",
24+
"mallocWrapper",
25+
"mutexEvents",
26+
"mutex",
27+
"access",
28+
"race",
29+
"escape",
30+
"expRelation",
31+
"mhp",
32+
"assert",
33+
"var_eq",
34+
"symb_locks",
35+
"region",
36+
"thread",
37+
"threadJoins",
38+
"abortUnless",
39+
"apron"
40+
],
41+
"apron":{
42+
"domain":"polyhedra"
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+
"callString_length":3,
56+
"gas_scope": "function",
57+
"gas_value":60
58+
},
59+
"base": {
60+
"arrays": {
61+
"domain": "unroll",
62+
"unrolling-factor": 128
63+
},
64+
"structs":{
65+
"domain": "sets"
66+
}
67+
},
68+
"race": {
69+
"free": false,
70+
"call": false
71+
},
72+
"autotune": {
73+
"enabled": true,
74+
"activated": [
75+
"reduceAnalyses",
76+
"mallocWrappers",
77+
"noRecursiveIntervals",
78+
"enums",
79+
"congruence",
80+
"wideningThresholds",
81+
"loopUnrollHeuristic",
82+
"memsafetySpecification",
83+
"noOverflows",
84+
"termination",
85+
"tmpSpecialAnalysis"
86+
]
87+
}
88+
},
89+
"exp": {
90+
"region-offsets": true,
91+
"unrolling-factor": 128
92+
},
93+
"solver": "td3",
94+
"solvers":{
95+
"td3":{
96+
"side_widen_gas":60,
97+
"widen_gas":60
98+
}
99+
},
100+
"sem": {
101+
"unknown_function": {
102+
"spawn": false
103+
},
104+
"int": {
105+
"signed_overflow": "assume_none"
106+
},
107+
"null-pointer": {
108+
"dereference": "assume_none"
109+
}
110+
},
111+
"witness": {
112+
"yaml": {
113+
"enabled": true,
114+
"format-version": "2.0",
115+
"entry-types": [
116+
"invariant_set"
117+
],
118+
"invariant-types": [
119+
"loop_invariant"
120+
]
121+
},
122+
"invariant": {
123+
"loop-head": true,
124+
"after-lock": false,
125+
"other": false,
126+
"accessed": false,
127+
"exact": true
128+
}
129+
},
130+
"pre": {
131+
"enabled": false
132+
}
133+
}

‎conf/svcomp26/seq.txt‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
# standard run based on svcomp 25 settings
2+
svcomp26/level00.json
3+
# next level proof of concept
4+
svcomp26/level01.json

0 commit comments

Comments
 (0)