Skip to content

Commit cea4416

Browse files
michael-schwarzmichael-schwarz
committed
Add two more configs
1 parent 4c2d8a3 commit cea4416

File tree

2 files changed

+256
-0
lines changed

2 files changed

+256
-0
lines changed

‎conf/race-digests/full-minus-region.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": 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+
"digests": {
58+
"lockset": true,
59+
"thread": true,
60+
"fresh": true,
61+
"region": false,
62+
"symb_locks": true,
63+
"threadflag": true,
64+
"tid": true,
65+
"join" : true
66+
}
67+
},
68+
"autotune": {
69+
"enabled": true,
70+
"activated": [
71+
"singleThreaded",
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+
"sem": {
91+
"unknown_function": {
92+
"spawn": false
93+
},
94+
"int": {
95+
"signed_overflow": "assume_none"
96+
},
97+
"null-pointer": {
98+
"dereference": "assume_none"
99+
}
100+
},
101+
"witness": {
102+
"graphml": {
103+
"enabled": true,
104+
"id": "enumerate",
105+
"unknown": false
106+
},
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+
}

‎conf/race-digests/mutex+threadflag.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": 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+
"digests": {
58+
"lockset": true,
59+
"thread": false,
60+
"fresh": false,
61+
"region": false,
62+
"symb_locks": false,
63+
"threadflag": true,
64+
"tid": false,
65+
"join" : false
66+
}
67+
},
68+
"autotune": {
69+
"enabled": true,
70+
"activated": [
71+
"singleThreaded",
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+
"sem": {
91+
"unknown_function": {
92+
"spawn": false
93+
},
94+
"int": {
95+
"signed_overflow": "assume_none"
96+
},
97+
"null-pointer": {
98+
"dereference": "assume_none"
99+
}
100+
},
101+
"witness": {
102+
"graphml": {
103+
"enabled": true,
104+
"id": "enumerate",
105+
"unknown": false
106+
},
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)