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 000000000000..e31a62ef61b4 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 000000000000..da813a5f3dee --- /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 000000000000..f894ebdb1e03 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 000000000000..b631e2e7617b --- /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 000000000000..4d40ffc37417 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 000000000000..6d80d3b38c54 --- /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 000000000000..4102562d05f5 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 000000000000..58ed13eaaa45 --- /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 000000000000..fa85a072b9f2 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 000000000000..ae5be7d1ecdb --- /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 000000000000..be106b10e2e9 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 000000000000..c2657791ddc3 --- /dev/null +++ b/regression/cbmc-java/array_nonconstsize_nonconstaccess/RefMultidimConstsize.java @@ -0,0 +1,10 @@ +public class RefMultidimConstsize { + public void f(int y) { + A[][] a1 = new A[2][2]; + if (y > 0) { + 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 000000000000..741443d1e2d2 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 000000000000..1237623d6f5b --- /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 000000000000..54c7ed67f46f --- /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 000000000000..6803953f5a2e --- /dev/null +++ b/regression/cbmc-java/array_nonconstsize_nonconstaccess/test_float_multidim_2.desc @@ -0,0 +1,6 @@ +CORE +FloatMultidim2.class +--function FloatMultidim2.f --cover location --unwind 3 +\d+ of \d+ covered \(100\.0\%\) +^EXIT=0$ +^SIGNAL=0$ 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 000000000000..f96f028e32ff --- /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 000000000000..190b154c371c --- /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 000000000000..272a1d579ebd --- /dev/null +++ b/regression/cbmc-java/array_nonconstsize_nonconstaccess/test_ref_multidim_constsize.desc @@ -0,0 +1,7 @@ +CORE +RefMultidimConstsize.class +--function RefMultidimConstsize.f --cover location --unwind 3 +^EXIT=0$ +^SIGNAL=0$ +-- +^\[java::RefMultidimConstsize\.f:\(I\)V.*\sFAILED$ 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 000000000000..de8b0da08ca6 --- /dev/null +++ b/regression/cbmc-java/array_nonconstsize_nonconstaccess/test_ref_singledim.desc @@ -0,0 +1,7 @@ +CORE +RefSingledim.class +--function RefSingledim.f --cover location --unwind 3 +^EXIT=0$ +^SIGNAL=0$ +-- +^\[java::RefSingledim\.f:\(I\)\[LA;.*\sFAILED$