Merge pull request diffblue#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;
+    }
+  }
+}

regression/cbmc-java/array_nonconstsize_nonconstaccess/FloatMultidim2.java

@@ -0,0 +1,8 @@
+public class RefMultidimConstsize {
+  public void f(int y) {
+    A[][] a1 = new A[2][2];
+    int j = 1;
+    a1[j][1] = new A();
+    a1[j][1].a = 1.0f;
+  }
+}

regression/cbmc-java/array_nonconstsize_nonconstaccess/RefMultidim1.class

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

regression/cbmc-java/array_nonconstsize_nonconstaccess/RefMultidim1.java

@@ -0,0 +1,12 @@
+KNOWNBUG
+FloatMultidim1.class
+--function FloatMultidim1.f --cover location --unwind 3
+\d+ of \d+ covered
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+This crashes during symex, with error 'cannot unpack array of nonconst size'
+when trying to access the element of the array. Symex uses byte_extract_little
+_endian to access the element which does not get simplified (it seems the
+problem is that the types in the instruction do not match). TG-1121

regression/cbmc-java/array_nonconstsize_nonconstaccess/RefMultidim2.class

@@ -0,0 +1,8 @@
+CORE
+FloatMultidim2.class
+--function FloatMultidim2.f --cover location --unwind 3
+^EXIT=0$
+^SIGNAL=0$
+y=1$
+y=[2-4]$
+y=([05-9]|[1-9][0-9]+|-[1-9][0-9]*)$

regression/cbmc-java/array_nonconstsize_nonconstaccess/RefMultidim2.java

@@ -0,0 +1,12 @@
+KNOWNBUG
+RefMultidim1.class
+--function RefMultidim1.f --cover location --unwind 3
+\d+ of \d+ covered
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+This crashes during symex, with error 'cannot unpack array of nonconst size'
+when trying to access the element of the array. Symex uses byte_extract_little
+_endian to access the element which does not get simplified (it seems the
+problem is that the types in the instruction do not match). TG-1121

regression/cbmc-java/array_nonconstsize_nonconstaccess/RefMultidimConstsize.class

@@ -0,0 +1,12 @@
+KNOWNBUG
+RefMultidim2.class
+--function RefMultidim2.f --cover location --unwind 3
+\d+ of \d+ covered
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+This crashes during symex, with error 'cannot unpack array of nonconst size'
+when trying to access the element of the array. Symex uses byte_extract_little
+_endian to access the element which does not get simplified (it seems the
+problem is that the types in the instruction do not match). TG-1121

regression/cbmc-java/array_nonconstsize_nonconstaccess/RefMultidimConstsize.java

@@ -0,0 +1,6 @@
+CORE
+RefMultidimConstsize.class
+--function RefMultidimConstsize.f --cover location --unwind 3
+^EXIT=0$
+^SIGNAL=0$
+y=-*[0-9]+$

regression/cbmc-java/array_nonconstsize_nonconstaccess/RefSingledim.class

@@ -0,0 +1,8 @@
+CORE
+RefSingledim.class
+--function RefSingledim.f --cover location --unwind 3
+^EXIT=0$
+^SIGNAL=0$
+y=1$
+y=[2-4]$
+y=([05-9]|[1-9][0-9]+|-[1-9][0-9]*)$