We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent 9e2811a commit 390aaddCopy full SHA for 390aadd
regression/cbmc-java/dynamic-multi-dimensional-array/TestClass.class
399 Bytes
regression/cbmc-java/dynamic-multi-dimensional-array/TestClass.java
@@ -0,0 +1,7 @@
1
+public class TestClass {
2
+ public static void f(int y) {
3
+ float[][] a1 = new float[y][3];
4
+ int j = 0;
5
+ a1[j][0] = 34.5f;
6
+ }
7
+}
regression/cbmc-java/dynamic-multi-dimensional-array/test.desc
@@ -0,0 +1,9 @@
+CORE
+TestClass.class
+--function TestClass.f --cover location --unwind 2
+Source GOTO statement: .*
+(^ exception: Can't convert byte_extraction|warning: Nested exception printing not supported on Windows)
+^EXIT=6$
+--
8
9
+This is a bug - this validates the error output.
0 commit comments