diff --git a/jbmc/regression/jbmc/array-clone/ArrayClone.class b/jbmc/regression/jbmc/array-clone/ArrayClone.class new file mode 100644 index 00000000000..2e985bf8761 Binary files /dev/null and b/jbmc/regression/jbmc/array-clone/ArrayClone.class differ diff --git a/jbmc/regression/jbmc/array-clone/ArrayClone.java b/jbmc/regression/jbmc/array-clone/ArrayClone.java new file mode 100644 index 00000000000..203c5e57872 --- /dev/null +++ b/jbmc/regression/jbmc/array-clone/ArrayClone.java @@ -0,0 +1,92 @@ +public class ArrayClone { + public static void cloneReferenceArray() { + ArrayClone[] a = {new ArrayClone(), new ArrayClone() }; + ArrayClone[] clone = a.clone(); + + assert(a.length == clone.length); + assert(a[0] == clone[0]); + assert(a[1] == clone[1]); + assert(a != clone); + } + + public static void cloneObjectArray() { + Object[] a = {new Object(), new Object() }; + Object[] clone = a.clone(); + + assert(a.length == clone.length); + assert(a[0] == clone[0]); + assert(a[1] == clone[1]); + assert(a != clone); + } + + public static void cloneByteArray() { + byte[] a = {(byte) 1, (byte) 2}; + byte[] clone = a.clone(); + + assert(a.length == clone.length); + assert(a[0] == clone[0]); + assert(a[1] == clone[1]); + assert(a != clone); + } + + public static void cloneShortArray() { + short[] a = {(short) 1, (short) 2}; + short[] clone = a.clone(); + + assert(a.length == clone.length); + assert(a[0] == clone[0]); + assert(a[1] == clone[1]); + assert(a != clone); + } + + public static void cloneIntArray() { + int[] a = {1, 2}; + int[] clone = a.clone(); + + assert(a.length == clone.length); + assert(a[0] == clone[0]); + assert(a[1] == clone[1]); + assert(a != clone); + } + + public static void cloneLongArray() { + long[] a = {1L, 2L }; + long[] clone = a.clone(); + + assert(a.length == clone.length); + assert(a[0] == clone[0]); + assert(a[1] == clone[1]); + assert(a != clone); + } + + public static void cloneFloatArray() { + float[] a = {1.0f, 2.0f}; + float[] clone = a.clone(); + + assert(a.length == clone.length); + assert(a[0] == clone[0]); + assert(a[1] == clone[1]); + assert(a != clone); + } + + public static void cloneDoubleArray() { + double[] a = {1.0, 2.0}; + double[] clone = a.clone(); + + assert(a.length == clone.length); + assert(a[0] == clone[0]); + assert(a[1] == clone[1]); + assert(a != clone); + } + + public static void cloneBooleanArray() { + boolean[] a = {true, false}; + boolean[] clone = a.clone(); + + assert(a.length == clone.length); + assert(a[0] == clone[0]); + assert(a[1] == clone[1]); + assert(a != clone); + } + +} diff --git a/jbmc/regression/jbmc/array-clone/testBoolean.desc b/jbmc/regression/jbmc/array-clone/testBoolean.desc new file mode 100644 index 00000000000..5585b05976d --- /dev/null +++ b/jbmc/regression/jbmc/array-clone/testBoolean.desc @@ -0,0 +1,9 @@ +CORE +ArrayClone.class +--function ArrayClone.cloneBooleanArray +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- +Verify that the clone works on a boolean array diff --git a/jbmc/regression/jbmc/array-clone/testByte.desc b/jbmc/regression/jbmc/array-clone/testByte.desc new file mode 100644 index 00000000000..cd6ab8e0252 --- /dev/null +++ b/jbmc/regression/jbmc/array-clone/testByte.desc @@ -0,0 +1,9 @@ +CORE +ArrayClone.class +--function ArrayClone.cloneByteArray +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- +Verify that clone works correctly for byte arrays diff --git a/jbmc/regression/jbmc/array-clone/testDouble.desc b/jbmc/regression/jbmc/array-clone/testDouble.desc new file mode 100644 index 00000000000..6c9367d8e1d --- /dev/null +++ b/jbmc/regression/jbmc/array-clone/testDouble.desc @@ -0,0 +1,9 @@ +CORE +ArrayClone.class +--function ArrayClone.cloneDoubleArray +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- +Verify that clone works correctly for double arrays diff --git a/jbmc/regression/jbmc/array-clone/testFloat.desc b/jbmc/regression/jbmc/array-clone/testFloat.desc new file mode 100644 index 00000000000..415c756cb98 --- /dev/null +++ b/jbmc/regression/jbmc/array-clone/testFloat.desc @@ -0,0 +1,9 @@ +CORE +ArrayClone.class +--function ArrayClone.cloneFloatArray +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- +Verify that clone works correctly for float arrays diff --git a/jbmc/regression/jbmc/array-clone/testInt.desc b/jbmc/regression/jbmc/array-clone/testInt.desc new file mode 100644 index 00000000000..d53ec5b6da8 --- /dev/null +++ b/jbmc/regression/jbmc/array-clone/testInt.desc @@ -0,0 +1,9 @@ +CORE +ArrayClone.class +--function ArrayClone.cloneIntArray +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- +Verify that clone works correctly for int arrays diff --git a/jbmc/regression/jbmc/array-clone/testLong.desc b/jbmc/regression/jbmc/array-clone/testLong.desc new file mode 100644 index 00000000000..b7f9de203de --- /dev/null +++ b/jbmc/regression/jbmc/array-clone/testLong.desc @@ -0,0 +1,9 @@ +CORE +ArrayClone.class +--function ArrayClone.cloneLongArray +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- +Verify that clone works correctly for long arrays diff --git a/jbmc/regression/jbmc/array-clone/testObject.desc b/jbmc/regression/jbmc/array-clone/testObject.desc new file mode 100644 index 00000000000..029b9691cc3 --- /dev/null +++ b/jbmc/regression/jbmc/array-clone/testObject.desc @@ -0,0 +1,9 @@ +CORE +ArrayClone.class +--function ArrayClone.cloneObjectArray +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- +Verify that clone works correctly for arrays of objects diff --git a/jbmc/regression/jbmc/array-clone/testReference.desc b/jbmc/regression/jbmc/array-clone/testReference.desc new file mode 100644 index 00000000000..bdf357436e7 --- /dev/null +++ b/jbmc/regression/jbmc/array-clone/testReference.desc @@ -0,0 +1,9 @@ +CORE +ArrayClone.class +--function ArrayClone.cloneReferenceArray +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- +Verify that clone works correctly for reference (non-object) arrays diff --git a/jbmc/regression/jbmc/array-clone/testShort.desc b/jbmc/regression/jbmc/array-clone/testShort.desc new file mode 100644 index 00000000000..2932bf15c2b --- /dev/null +++ b/jbmc/regression/jbmc/array-clone/testShort.desc @@ -0,0 +1,9 @@ +CORE +ArrayClone.class +--function ArrayClone.cloneShortArray +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- +Verify that clone works correctly for short arrays diff --git a/jbmc/src/java_bytecode/ci_lazy_methods_needed.cpp b/jbmc/src/java_bytecode/ci_lazy_methods_needed.cpp index 620e874dda8..db19734fddb 100644 --- a/jbmc/src/java_bytecode/ci_lazy_methods_needed.cpp +++ b/jbmc/src/java_bytecode/ci_lazy_methods_needed.cpp @@ -138,7 +138,9 @@ void ci_lazy_methods_neededt::gather_field_types( { const typet &element_type = java_array_element_type(to_struct_tag_type(class_type)); - if(element_type.id() == ID_pointer) + if( + element_type.id() == ID_pointer && + element_type.subtype().id() != ID_empty) { // This is a reference array -- mark its element type available. add_all_needed_classes(to_pointer_type(element_type));