forked from vorpal-research/kex
-
Notifications
You must be signed in to change notification settings - Fork 0
/
kex.ini
109 lines (90 loc) · 1.89 KB
/
kex.ini
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
;suppress inspection "DuplicateKeyInSection" for whole file
[kex]
libPath = runtime-deps/lib/
rtVersion = 1.8
kexRtVersion = 0.0.1
intrinsicsVersion = 0.0.7
junitVersion = 4.12
outputDir = temp/
testsDir = tests/
useJavaRuntime = true
useKexRuntime = true
[compile]
compileDir = compiled/
[easy-random]
depth = 10
minCollectionSize = 0
maxCollectionSize = 10
minStringLength = 0
maxStringLength = 10
generationAttempts = 100
ignoreErrors = true
bypassSetters = true
ignoreFieldInitializationErrors = true
exclude = java.sql.SQLException
exclude = com.sun.xml.*
exclude = com.fasterxml.jackson.*
exclude = sun.*
exclude = com.github.luben.*
exclude = org.jetbrains.research.smt.*
exclude = net.sf.saxon.*
exclude = java.lang.Thread
[runner]
timeout = 10000
[concolic]
timeLimit = 500000
maxFailsInARow = 50
searchStrategy = cgs
[random-runner]
enabled = false
attempts = 10
[inliner]
enabled = true
depth = 3
irInlining = false
ignorePackage = java.util.*
ignorePackage = java.lang.*
ignoreClass = org.jetbrains.research.kex.test.Intrinsics
ignoreClass = kotlin.jvm.internal.Intrinsics
[annotations]
enabled = true
path = runtime-deps/annotations/
printAnnotationInfo = false
[loop]
derollCount = 1
maxDerollCount = 1
[smt]
engine = z3
timeout = 5
defaultAllocationSize = 512
psInlining = true
memspacing = false
slicing = false
logQuery = true
logFormulae = false
logSMTLib = false
simplifyFormulae = false
[z3]
tacticsFile = runtime-deps/z3.tactics
paramFile = runtime-deps/z3.params
[view]
dot = /usr/bin/dot
viewer = /usr/bin/google-chrome-stable
[debug]
dump-directory = fails
[apiGeneration]
enabled = true
useConcreteImpl = true
visibility = public
recursiveInlining = false
maxStackSize = 5
useSetters = false
maxQuerySize = 1000
maxSearchDepth = 1000
maxGenerationDepth = 100
maxConversionDepth = 10
generateTestCases = true
testCaseLanguage = java
generateSetup = true
[defect]
outputFile = defects.json