diff --git a/regression/cbmc-java/array_nonconstsize_nonconstaccess/A.class b/regression/cbmc-java/array_nonconstsize_nonconstaccess/A.class new file mode 100644 index 00000000000..e31a62ef61b Binary files /dev/null and b/regression/cbmc-java/array_nonconstsize_nonconstaccess/A.class differ diff --git a/regression/cbmc-java/array_nonconstsize_nonconstaccess/A.java b/regression/cbmc-java/array_nonconstsize_nonconstaccess/A.java new file mode 100644 index 00000000000..da813a5f3de --- /dev/null +++ b/regression/cbmc-java/array_nonconstsize_nonconstaccess/A.java @@ -0,0 +1,3 @@ +public class A { + public float a; +} diff --git a/regression/cbmc-java/array_nonconstsize_nonconstaccess/FloatMultidim1.class b/regression/cbmc-java/array_nonconstsize_nonconstaccess/FloatMultidim1.class new file mode 100644 index 00000000000..f894ebdb1e0 Binary files /dev/null and b/regression/cbmc-java/array_nonconstsize_nonconstaccess/FloatMultidim1.class differ diff --git a/regression/cbmc-java/array_nonconstsize_nonconstaccess/FloatMultidim1.java b/regression/cbmc-java/array_nonconstsize_nonconstaccess/FloatMultidim1.java new file mode 100644 index 00000000000..b631e2e7617 --- /dev/null +++ b/regression/cbmc-java/array_nonconstsize_nonconstaccess/FloatMultidim1.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; + } + } +} diff --git a/regression/cbmc-java/array_nonconstsize_nonconstaccess/FloatMultidim2.class b/regression/cbmc-java/array_nonconstsize_nonconstaccess/FloatMultidim2.class new file mode 100644 index 00000000000..4d40ffc3741 Binary files /dev/null and b/regression/cbmc-java/array_nonconstsize_nonconstaccess/FloatMultidim2.class differ diff --git a/regression/cbmc-java/array_nonconstsize_nonconstaccess/FloatMultidim2.java b/regression/cbmc-java/array_nonconstsize_nonconstaccess/FloatMultidim2.java new file mode 100644 index 00000000000..6d80d3b38c5 --- /dev/null +++ b/regression/cbmc-java/array_nonconstsize_nonconstaccess/FloatMultidim2.java @@ -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]; + } + } +} diff --git a/regression/cbmc-java/array_nonconstsize_nonconstaccess/RefMultidim1.class b/regression/cbmc-java/array_nonconstsize_nonconstaccess/RefMultidim1.class new file mode 100644 index 00000000000..4102562d05f Binary files /dev/null and b/regression/cbmc-java/array_nonconstsize_nonconstaccess/RefMultidim1.class differ diff --git a/regression/cbmc-java/array_nonconstsize_nonconstaccess/RefMultidim1.java b/regression/cbmc-java/array_nonconstsize_nonconstaccess/RefMultidim1.java new file mode 100644 index 00000000000..58ed13eaaa4 --- /dev/null +++ b/regression/cbmc-java/array_nonconstsize_nonconstaccess/RefMultidim1.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; + } + } +} diff --git a/regression/cbmc-java/array_nonconstsize_nonconstaccess/RefMultidim2.class b/regression/cbmc-java/array_nonconstsize_nonconstaccess/RefMultidim2.class new file mode 100644 index 00000000000..fa85a072b9f Binary files /dev/null and b/regression/cbmc-java/array_nonconstsize_nonconstaccess/RefMultidim2.class differ diff --git a/regression/cbmc-java/array_nonconstsize_nonconstaccess/RefMultidim2.java b/regression/cbmc-java/array_nonconstsize_nonconstaccess/RefMultidim2.java new file mode 100644 index 00000000000..ae5be7d1ecd --- /dev/null +++ b/regression/cbmc-java/array_nonconstsize_nonconstaccess/RefMultidim2.java @@ -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; + } + } +} diff --git a/regression/cbmc-java/array_nonconstsize_nonconstaccess/RefMultidimConstsize.class b/regression/cbmc-java/array_nonconstsize_nonconstaccess/RefMultidimConstsize.class new file mode 100644 index 00000000000..c474465f50d Binary files /dev/null and b/regression/cbmc-java/array_nonconstsize_nonconstaccess/RefMultidimConstsize.class differ diff --git a/regression/cbmc-java/array_nonconstsize_nonconstaccess/RefMultidimConstsize.java b/regression/cbmc-java/array_nonconstsize_nonconstaccess/RefMultidimConstsize.java new file mode 100644 index 00000000000..90692e0392a --- /dev/null +++ b/regression/cbmc-java/array_nonconstsize_nonconstaccess/RefMultidimConstsize.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; + } +} diff --git a/regression/cbmc-java/array_nonconstsize_nonconstaccess/RefSingledim.class b/regression/cbmc-java/array_nonconstsize_nonconstaccess/RefSingledim.class new file mode 100644 index 00000000000..741443d1e2d Binary files /dev/null and b/regression/cbmc-java/array_nonconstsize_nonconstaccess/RefSingledim.class differ diff --git a/regression/cbmc-java/array_nonconstsize_nonconstaccess/RefSingledim.java b/regression/cbmc-java/array_nonconstsize_nonconstaccess/RefSingledim.java new file mode 100644 index 00000000000..1237623d6f5 --- /dev/null +++ b/regression/cbmc-java/array_nonconstsize_nonconstaccess/RefSingledim.java @@ -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; + } + } +} diff --git a/regression/cbmc-java/array_nonconstsize_nonconstaccess/test_float_multidim_1.desc b/regression/cbmc-java/array_nonconstsize_nonconstaccess/test_float_multidim_1.desc new file mode 100644 index 00000000000..54c7ed67f46 --- /dev/null +++ b/regression/cbmc-java/array_nonconstsize_nonconstaccess/test_float_multidim_1.desc @@ -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 diff --git a/regression/cbmc-java/array_nonconstsize_nonconstaccess/test_float_multidim_2.desc b/regression/cbmc-java/array_nonconstsize_nonconstaccess/test_float_multidim_2.desc new file mode 100644 index 00000000000..9f1c5d4581b --- /dev/null +++ b/regression/cbmc-java/array_nonconstsize_nonconstaccess/test_float_multidim_2.desc @@ -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]*)$ diff --git a/regression/cbmc-java/array_nonconstsize_nonconstaccess/test_ref_multidim_1.desc b/regression/cbmc-java/array_nonconstsize_nonconstaccess/test_ref_multidim_1.desc new file mode 100644 index 00000000000..f96f028e32f --- /dev/null +++ b/regression/cbmc-java/array_nonconstsize_nonconstaccess/test_ref_multidim_1.desc @@ -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 diff --git a/regression/cbmc-java/array_nonconstsize_nonconstaccess/test_ref_multidim_2.desc b/regression/cbmc-java/array_nonconstsize_nonconstaccess/test_ref_multidim_2.desc new file mode 100644 index 00000000000..190b154c371 --- /dev/null +++ b/regression/cbmc-java/array_nonconstsize_nonconstaccess/test_ref_multidim_2.desc @@ -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 diff --git a/regression/cbmc-java/array_nonconstsize_nonconstaccess/test_ref_multidim_constsize.desc b/regression/cbmc-java/array_nonconstsize_nonconstaccess/test_ref_multidim_constsize.desc new file mode 100644 index 00000000000..eeb64c3e6b1 --- /dev/null +++ b/regression/cbmc-java/array_nonconstsize_nonconstaccess/test_ref_multidim_constsize.desc @@ -0,0 +1,6 @@ +CORE +RefMultidimConstsize.class +--function RefMultidimConstsize.f --cover location --unwind 3 +^EXIT=0$ +^SIGNAL=0$ +y=-*[0-9]+$ diff --git a/regression/cbmc-java/array_nonconstsize_nonconstaccess/test_ref_singledim.desc b/regression/cbmc-java/array_nonconstsize_nonconstaccess/test_ref_singledim.desc new file mode 100644 index 00000000000..84db685c705 --- /dev/null +++ b/regression/cbmc-java/array_nonconstsize_nonconstaccess/test_ref_singledim.desc @@ -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]*)$