|
1 |
| -# This file has been automatically pushed to all dashboard benchmarks (except for Java Demo). |
2 |
| -# All changes made to this file should be propagated to all dashboard benchmarks. Do not change this file individually! |
| 1 | +# This file was automatically generated using script in dashboard/scripts/update-diffblue-yml |
| 2 | +# It is a combination of the diffblue-base.yml from the project repository and a custom yml file |
| 3 | +# Do not change any of the values manually to keep options uniform across all benchmarks |
3 | 4 | skipVerification: true
|
4 | 5 | cbmcArguments:
|
5 | 6 | java-max-vla-length: 100000
|
6 | 7 | phases:
|
7 |
| -- |
8 |
| -#0 Pretty tests. If timeout then go to #3 |
9 |
| - timeout: 300 |
10 |
| - cbmcArguments: |
11 |
| - classpath: '/tools/cbmc/models-simple-overlay.jar:/tools/cbmc/models.jar:.' |
12 |
| - depth: 1500 |
13 |
| - java-assume-inputs-non-null: true |
14 |
| - max-nondet-array-length: 10 |
15 |
| - max-nondet-string-length: 10 |
16 |
| - string-printable: true |
17 |
| - throw-runtime-exceptions: false |
18 |
| - unwind: 1 |
19 |
| - nextPhase: |
20 |
| - not_analyzed: null |
21 |
| - time_out: 3 |
22 |
| -- |
23 |
| -#1 Increased values, allow null. If timeout then go to #3 |
24 |
| - timeout: 300 |
25 |
| - cbmcArguments: |
26 |
| - classpath: '/tools/cbmc/models-simple-overlay.jar:/tools/cbmc/models.jar:.' |
27 |
| - depth: 1500 |
28 |
| - java-assume-inputs-non-null: false |
29 |
| - max-nondet-array-length: 20 |
30 |
| - max-nondet-string-length: 50 |
31 |
| - string-printable: true |
32 |
| - throw-runtime-exceptions: false |
33 |
| - unwind: 2 |
34 |
| - nextPhase: |
35 |
| - time_out: 3 |
36 |
| -- |
37 |
| -#2 Increased values, allow exceptions |
38 |
| - timeout: 300 |
39 |
| - cbmcArguments: |
40 |
| - classpath: '/tools/cbmc/models.jar:.' |
41 |
| - depth: 3000 |
42 |
| - java-assume-inputs-non-null: false |
43 |
| - max-nondet-array-length: 30 |
44 |
| - max-nondet-string-length: 100 |
45 |
| - string-printable: false |
46 |
| - throw-runtime-exceptions: true |
47 |
| - unwind: 3 |
48 |
| -- |
49 |
| -#3 Fallback phase - copy of #2 with single-path symex, unbounded unwind and depth, lower timeout |
50 |
| - timeout: 100 |
51 |
| - cbmcArguments: |
52 |
| - classpath: '/tools/cbmc/models.jar:.' |
53 |
| - depth: false |
54 |
| - java-assume-inputs-non-null: false |
55 |
| - max-nondet-array-length: 30 |
56 |
| - max-nondet-string-length: 100 |
57 |
| - paths: 'fifo' |
58 |
| - string-printable: false |
59 |
| - throw-runtime-exceptions: true |
60 |
| - unwind: false |
61 |
| -- |
62 |
| -#4 Fallback phase - copy of #0 with load-containing-class-only |
63 |
| - timeout: 300 |
64 |
| - cbmcArguments: |
65 |
| - classpath: '/tools/cbmc/models-simple-overlay.jar:/tools/cbmc/models.jar:.' |
66 |
| - depth: 1500 |
67 |
| - java-assume-inputs-non-null: true |
68 |
| - load-containing-class-only: true |
69 |
| - max-nondet-array-length: 10 |
70 |
| - max-nondet-string-length: 10 |
71 |
| - string-printable: true |
72 |
| - throw-runtime-exceptions: false |
73 |
| - unwind: 1 |
74 |
| -- |
75 |
| -#5 Fallback phase - copy of #2 with load-containing-class-only |
76 |
| - timeout: 300 |
77 |
| - cbmcArguments: |
78 |
| - classpath: '/tools/cbmc/models.jar:.' |
79 |
| - depth: 3000 |
80 |
| - java-assume-inputs-non-null: false |
81 |
| - load-containing-class-only: true |
82 |
| - max-nondet-array-length: 30 |
83 |
| - max-nondet-string-length: 100 |
84 |
| - string-printable: false |
85 |
| - throw-runtime-exceptions: true |
86 |
| - unwind: 3 |
87 |
| -- |
88 |
| -#6 Fallback phase - copy of #0 with single-function-only |
89 |
| - timeout: 300 |
90 |
| - cbmcArguments: |
91 |
| - classpath: '/tools/cbmc/models-simple-overlay.jar:/tools/cbmc/models.jar:.' |
92 |
| - depth: 1500 |
93 |
| - java-assume-inputs-non-null: true |
94 |
| - max-nondet-array-length: 10 |
95 |
| - max-nondet-string-length: 10 |
96 |
| - single-function-only: true |
97 |
| - string-printable: true |
98 |
| - throw-runtime-exceptions: false |
99 |
| - unwind: 1 |
100 |
| -- |
101 |
| -#7 Fallback phase - copy of #2 with single-function-only |
102 |
| - timeout: 300 |
103 |
| - cbmcArguments: |
104 |
| - classpath: '/tools/cbmc/models.jar:.' |
105 |
| - depth: 3000 |
106 |
| - java-assume-inputs-non-null: false |
107 |
| - max-nondet-array-length: 30 |
108 |
| - max-nondet-string-length: 100 |
109 |
| - single-function-only: true |
110 |
| - string-printable: false |
111 |
| - throw-runtime-exceptions: true |
112 |
| - unwind: 3 |
| 8 | + - timeout: 300 |
| 9 | + cbmcArguments: |
| 10 | + classpath: '/tools/cbmc/models-simple-overlay.jar:/tools/cbmc/models.jar:.' |
| 11 | + depth: 1500 |
| 12 | + java-assume-inputs-non-null: true |
| 13 | + max-nondet-array-length: 10 |
| 14 | + max-nondet-string-length: 10 |
| 15 | + string-printable: true |
| 16 | + throw-runtime-exceptions: false |
| 17 | + unwind: 1 |
| 18 | + nextPhase: |
| 19 | + not_analyzed: null |
| 20 | + time_out: 3 |
| 21 | + - timeout: 300 |
| 22 | + cbmcArguments: |
| 23 | + classpath: '/tools/cbmc/models-simple-overlay.jar:/tools/cbmc/models.jar:.' |
| 24 | + depth: 1500 |
| 25 | + java-assume-inputs-non-null: false |
| 26 | + max-nondet-array-length: 20 |
| 27 | + max-nondet-string-length: 50 |
| 28 | + string-printable: true |
| 29 | + throw-runtime-exceptions: false |
| 30 | + unwind: 2 |
| 31 | + nextPhase: |
| 32 | + time_out: 3 |
| 33 | + - timeout: 300 |
| 34 | + cbmcArguments: |
| 35 | + classpath: '/tools/cbmc/models.jar:.' |
| 36 | + depth: 3000 |
| 37 | + java-assume-inputs-non-null: false |
| 38 | + max-nondet-array-length: 30 |
| 39 | + max-nondet-string-length: 100 |
| 40 | + string-printable: false |
| 41 | + throw-runtime-exceptions: true |
| 42 | + unwind: 3 |
| 43 | + - timeout: 100 |
| 44 | + cbmcArguments: |
| 45 | + classpath: '/tools/cbmc/models.jar:.' |
| 46 | + depth: false |
| 47 | + java-assume-inputs-non-null: false |
| 48 | + max-nondet-array-length: 30 |
| 49 | + max-nondet-string-length: 100 |
| 50 | + paths: fifo |
| 51 | + string-printable: false |
| 52 | + throw-runtime-exceptions: true |
| 53 | + unwind: false |
| 54 | + - timeout: 300 |
| 55 | + cbmcArguments: |
| 56 | + classpath: '/tools/cbmc/models-simple-overlay.jar:/tools/cbmc/models.jar:.' |
| 57 | + depth: 1500 |
| 58 | + java-assume-inputs-non-null: true |
| 59 | + load-containing-class-only: true |
| 60 | + max-nondet-array-length: 10 |
| 61 | + max-nondet-string-length: 10 |
| 62 | + string-printable: true |
| 63 | + throw-runtime-exceptions: false |
| 64 | + unwind: 1 |
| 65 | + - timeout: 300 |
| 66 | + cbmcArguments: |
| 67 | + classpath: '/tools/cbmc/models.jar:.' |
| 68 | + depth: 3000 |
| 69 | + java-assume-inputs-non-null: false |
| 70 | + load-containing-class-only: true |
| 71 | + max-nondet-array-length: 30 |
| 72 | + max-nondet-string-length: 100 |
| 73 | + string-printable: false |
| 74 | + throw-runtime-exceptions: true |
| 75 | + unwind: 3 |
| 76 | + - timeout: 300 |
| 77 | + cbmcArguments: |
| 78 | + classpath: '/tools/cbmc/models-simple-overlay.jar:/tools/cbmc/models.jar:.' |
| 79 | + depth: 1500 |
| 80 | + java-assume-inputs-non-null: true |
| 81 | + max-nondet-array-length: 10 |
| 82 | + max-nondet-string-length: 10 |
| 83 | + single-function-only: true |
| 84 | + string-printable: true |
| 85 | + throw-runtime-exceptions: false |
| 86 | + unwind: 1 |
| 87 | + - timeout: 300 |
| 88 | + cbmcArguments: |
| 89 | + classpath: '/tools/cbmc/models.jar:.' |
| 90 | + depth: 3000 |
| 91 | + java-assume-inputs-non-null: false |
| 92 | + max-nondet-array-length: 30 |
| 93 | + max-nondet-string-length: 100 |
| 94 | + single-function-only: true |
| 95 | + string-printable: false |
| 96 | + throw-runtime-exceptions: true |
| 97 | + unwind: 3 |
0 commit comments