File tree Expand file tree Collapse file tree 3 files changed +29
-0
lines changed
jbmc/regression/jbmc/multidimensional-array-char Expand file tree Collapse file tree 3 files changed +29
-0
lines changed Original file line number Diff line number Diff line change
1
+ public class My {
2
+ public int check2DCharArray (char [][] board , boolean assertionCheck ) {
3
+ int diff = 0 ;
4
+ for (int row = 0 ; row < 2 ; row ++) {
5
+ for (int col = 0 ; col < 2 ; col ++) {
6
+ if (board [row ][col ] == 'O' ) {
7
+ diff ++;
8
+ assert !assertionCheck ;
9
+ } else if (board [row ][col ] == 'X' ) {
10
+ diff --;
11
+ assert !assertionCheck ;
12
+ }
13
+ }
14
+ }
15
+ return 0 ;
16
+ }
17
+ }
Original file line number Diff line number Diff line change
1
+ CORE
2
+ My.class
3
+ --function My.check2DCharArray --unwind 5 --max-nondet-array-length 10
4
+ line 8 assertion at file My.java.*: FAILURE
5
+ line 11 assertion at file My.java.*: FAILURE
6
+ ^VERIFICATION FAILED$
7
+ ^EXIT=10$
8
+ ^SIGNAL=0$
9
+ --
10
+ --
11
+ Multidimentional char array used to cause a performance issue (test-gen 0.8.1).
12
+ This was reported in TG-5076. The issue is no longer reproducible 0.9.0+.
You can’t perform that action at this time.
0 commit comments