Merge pull request #2119 from svorenova/gs_tg1121_regression

Adding regression tests for multi-dimensional arrays [TG-1121]

Author: Daniel Kroening

regression/cbmc-java/array_nonconstsize_nonconstaccess/A.class

@@ -0,0 +1,3 @@
+public class A {
+  public float a;
+}

regression/cbmc-java/array_nonconstsize_nonconstaccess/A.java

@@ -0,0 +1,17 @@
+public class FloatMultidim1 {
+  public float[][] f(int y) {
+    if (y > 0 && y < 5) {
+      float[][] a1 = new float[y][2];
+      int j;
+      if (y > 1) {
+        j = 1;
+      } else {
+        j = 0;
+      }
+      a1[j][1] = 1.0f;
+      return a1;
+    } else {
+      return null;
+    }
+  }
+}

regression/cbmc-java/array_nonconstsize_nonconstaccess/FloatMultidim1.class

@@ -0,0 +1,17 @@
+public class FloatMultidim2 {
+  public float[][] f(int y) {
+    if (y > 0 && y < 5) {
+      float[][] a1 = new float[2][y];
+      int j;
+      if (y > 1) {
+        j = 1;
+      } else {
+        j = 0;
+      }
+      a1[1][j] = 1.0f;
+      return a1;
+    } else {
+      return new float[1][1];
+    }
+  }
+}

regression/cbmc-java/array_nonconstsize_nonconstaccess/FloatMultidim1.java

@@ -0,0 +1,18 @@
+public class RefMultidim1 {
+  public A[][] f(int y) {
+    if (y > 0 && y < 5) {
+      A[][] a1 = new A[y][2];
+      int j;
+      if (y > 1) {
+        j = 1;
+      } else {
+        j = 0;
+      }
+      a1[j][1] = new A();
+      a1[j][1].a = 1.0f;
+      return a1;
+    } else {
+      return null;
+    }
+  }
+}

regression/cbmc-java/array_nonconstsize_nonconstaccess/FloatMultidim2.class

@@ -0,0 +1,18 @@
+public class RefMultidim2 {
+  public A[][] f(int y) {
+    if (y > 0 && y < 5) {
+      A[][] a1 = new A[2][y];
+      int j;
+      if (y > 1) {
+        j = 1;
+      } else {
+        j = 0;
+      }
+      a1[1][j] = new A();
+      a1[1][j].a = 1.0f;
+      return a1;
+    } else {
+      return null;
+    }
+  }
+}