forked from vorpal-research/kex
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathkex.ini
101 lines (82 loc) · 1.82 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
;suppress inspection "DuplicateKeyInSection" for whole file
[kex]
rtVersion = 1.8
rtPath = lib/
[easy-random]
depth = 10
minCollectionSize = 0
maxCollectionSize = 10
minStringLength = 0
maxStringLength = 10
generationAttempts = 100
exclude = java.sql.SQLException
exclude = com.sun.xml.*
exclude = com.fasterxml.jackson.*
exclude = sun.*
exclude = com.github.luben.*
exclude = org.jetbrains.research.smt.*
[runner]
timeout = 10000
[concolic]
timeLimit = 50000
main-only = false
[random-runner]
enabled = false
attempts = 10
[inliner]
enabled = true
depth = 3
ir-inlining = false
static-ignore = java.lang.CharacterDataLatin1
static-ignore = java.lang.CharacterData00
static-ignore = java.lang.CharacterData01
static-ignore = java.lang.CharacterData02
static-ignore = java.lang.CharacterDataUndefined
static-ignore = java.lang.CharacterData0E
static-ignore = java.lang.CharacterDataPrivateUse
ignore = org.jetbrains.research.kex.test.Intrinsics
ignore = kotlin.jvm.internal.Intrinsics
ignore = java.util.concurrent.*
ignore = java.util.HashMap
ignore = java.util.TreeMap
[annotations]
enabled = true
path = ./annotations
printAnnotationInfo = false
[loop]
deroll-count = 1
max-deroll-count = 1
[smt]
engine = z3
timeout = 5
defaultAllocationSize = 512
ps-inlining = true
memspacing = true
slicing = true
logQuery = true
logFormulae = false
logSMTLib = false
simplifyFormulae = true
[z3]
tacticsFile = z3.tactics
paramFile = z3.params
[view]
dot = /usr/bin/dot
viewer = /usr/bin/chromium
[debug]
dump-directory = ./fails
[apiGeneration]
enabled = true
use-concrete-impl = true
visibility = public
recursiveInlining = false
maxStackSize = 5
maxQuerySize = 1000
maxSearchDepth = 1000
maxGenerationDepth = 100
maxConversionDepth = 10
generateTestCases = true
testCaseDirectory= ./tests
testCaseLanguage = java
[defect]
outputFile = ./defects.json