Merge pull request diffblue#312 from diffblue/pull-support-20180112

Pull support 20180112

Author: NathanJPhillips

regression/cbmc-java/instanceof8/InstanceOf8.class

@@ -0,0 +1,14 @@
+public class InstanceOf8 {
+  public static boolean test(Integer i) {
+    if (i instanceof Integer) {
+      return true;
+    } else {
+      return false;
+    }
+  }
+  public static void main(String[] args)
+  {
+    assert(!test(null));
+    assert(test(new Integer(1)));
+  }
+}

regression/cbmc-java/instanceof8/InstanceOf8.java

@@ -0,0 +1,7 @@
+CORE
+InstanceOf8.class
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--

regression/cbmc-java/instanceof8/test.desc

@@ -0,0 +1,7 @@
+CORE
+test.class
+--lazy-methods --verbosity 10 --function test.g
+^EXIT=0$
+^SIGNAL=0$
+elaborate java::test\.f:\(\)I
+VERIFICATION SUCCESSFUL

regression/cbmc-java/lazyloading_array_parameter/asserthere.class

@@ -0,0 +1,22 @@
+
+public class test {
+
+  public int f() { return 1; }
+
+  public static void g(test[] args) {
+
+    if(args == null || args.length != 1 || args[0] == null)
+      return;
+    asserthere.doassert(args[0].f() == 1);
+
+  }
+
+}
+
+class asserthere {
+
+  // Used to avoid lazy-loading currently marking any class with an
+  // $assertionsEnabled member (i.e. any class that asserts) as needed.
+  public static void doassert(boolean condition) { assert(condition); }
+
+}

regression/cbmc-java/lazyloading_array_parameter/test.class

@@ -0,0 +1,7 @@
+CORE
+test.class
+--lazy-methods --verbosity 10 --function test.g
+^EXIT=0$
+^SIGNAL=0$
+elaborate java::test\.f:\(\)I
+VERIFICATION SUCCESSFUL

regression/cbmc-java/lazyloading_array_parameter/test.desc

@@ -0,0 +1,29 @@
+
+public class test {
+
+  public int f() { return 1; }
+
+  public static void g(container c) {
+
+    if(c == null)
+      return;
+    test[] args = c.test_array;
+    if(args == null || args.length != 1 || args[0] == null)
+      return;
+    asserthere.doassert(args[0].f() == 1);
+
+  }
+
+}
+
+class container {
+  public test[] test_array;
+}
+
+class asserthere {
+
+  // Used to avoid lazy-loading currently marking any class with an
+  // $assertionsEnabled member (i.e. any class that asserts) as needed.
+  public static void doassert(boolean condition) { assert(condition); }
+
+}

regression/cbmc-java/lazyloading_array_parameter/test.java

@@ -0,0 +1,7 @@
+CORE
+test.class
+--lazy-methods --verbosity 10 --function test.g
+^EXIT=0$
+^SIGNAL=0$
+elaborate java::test\.f:\(\)I
+VERIFICATION SUCCESSFUL

regression/cbmc-java/lazyloading_indirect_array_parameter/asserthere.class

@@ -0,0 +1,29 @@
+
+public class test {
+
+  public int f() { return 1; }
+
+  public static void g(container<test> c) {
+
+    if(c == null)
+      return;
+    test[] args = c.test_array;
+    if(args == null || args.length != 1 || args[0] == null)
+      return;
+    asserthere.doassert(args[0].f() == 1);
+
+  }
+
+}
+
+class container<T> {
+  public T[] test_array;
+}
+
+class asserthere {
+
+  // Used to avoid lazy-loading currently marking any class with an
+  // $assertionsEnabled member (i.e. any class that asserts) as needed.
+  public static void doassert(boolean condition) { assert(condition); }
+
+}

regression/cbmc-java/lazyloading_indirect_array_parameter/container.class

@@ -0,0 +1,7 @@
+CORE
+test.class
+--lazy-methods --verbosity 10 --function test.g
+^EXIT=0$
+^SIGNAL=0$
+elaborate java::test\.f:\(\)I
+VERIFICATION SUCCESSFUL

regression/cbmc-java/lazyloading_indirect_array_parameter/test.class

@@ -0,0 +1,29 @@
+
+public class test {
+
+  public int f() { return 1; }
+
+  public static void g(container<Integer, test> c) {
+
+    if(c == null)
+      return;
+    test[] args = c.test_array;
+    if(args == null || args.length != 1 || args[0] == null)
+      return;
+    asserthere.doassert(args[0].f() == 1);
+
+  }
+
+}
+
+class container<S, T> {
+  public T[] test_array;
+}
+
+class asserthere {
+
+  // Used to avoid lazy-loading currently marking any class with an
+  // $assertionsEnabled member (i.e. any class that asserts) as needed.
+  public static void doassert(boolean condition) { assert(condition); }
+
+}

regression/cbmc-java/lazyloading_indirect_array_parameter/test.desc

@@ -0,0 +1,13 @@
+KNOWNBUG
+test.class
+--lazy-methods --verbosity 10 --function test.g
+^EXIT=0$
+^SIGNAL=0$
+elaborate java::test\.f:\(\)I
+VERIFICATION SUCCESSFUL
+--
+--
+The right methods are loaded, but verification is not successful
+because __CPROVER_start doesn't create appropriately typed input for
+this kind of nested generic parameter, so dynamic cast checks fail upon
+fetching the generic type's field.

regression/cbmc-java/lazyloading_indirect_array_parameter/test.java

@@ -0,0 +1,36 @@
+
+public class test {
+
+  public int f() { return 1; }
+
+  public static void g(container2<container<test>> c) {
+
+    if(c == null)
+      return;
+    container<test> outer = c.next;
+    if(outer == null)
+      return;
+    test[] args = outer.test_array;
+    if(args == null || args.length != 1 || args[0] == null)
+      return;
+    asserthere.doassert(args[0].f() == 1);
+
+  }
+
+}
+
+class container<T> {
+  public T[] test_array;
+}
+
+class container2<T> {
+  public T next;
+}
+
+class asserthere {
+
+  // Used to avoid lazy-loading currently marking any class with an
+  // $assertionsEnabled member (i.e. any class that asserts) as needed.
+  public static void doassert(boolean condition) { assert(condition); }
+
+}

regression/cbmc-java/lazyloading_indirect_generic_array_parameter/asserthere.class

@@ -0,0 +1,42 @@
+public abstract class AbstractList<E>
+    implements List<E>
+{
+    public Iterator<E> iterator() {
+        return new Itr();
+    }
+
+    public ListIterator<E> listIterator() {
+        return listIterator(0);
+    }
+
+    public boolean equals(Object o) {
+        if (o == this)
+            return true;
+        if (!(o instanceof List))
+            return false;
+        
+        ListIterator<E> e1 = listIterator();
+        ListIterator<?> e2 = ((List<?>) o).listIterator();
+        while (e1.hasNext() && e2.hasNext()) {
+            E o1 = e1.next();
+            Object o2 = e2.next();
+            if (!(o1==null ? o2==null : o1.equals(o2)))
+                return false;
+        }
+        return !(e1.hasNext() || e2.hasNext());
+    }
+
+    private class Itr implements Iterator<E> {
+        Itr() {
+        }
+
+        public boolean hasNext() {
+            return false;
+        }
+
+        public E next() {
+            return null;
+        }
+            
+    }
+}

regression/cbmc-java/lazyloading_indirect_generic_array_parameter/container.class

@@ -0,0 +1,31 @@
+public class ArrayList<E> extends AbstractList<E>
+    implements List<E>
+{
+    public ListIterator<E> listIterator() {
+        return new ListItr(0);
+    }
+    public ListIterator<E> listIterator(int index) {
+        return new ListItr(index);
+    }
+    private class ListItr extends Itr implements ListIterator<E> {
+        ListItr(int index) {
+            super();
+        }
+
+        public boolean hasPrevious() {
+            return false;
+        }
+    }
+
+    private class Itr implements Iterator<E> {
+        Itr() {
+        }
+
+        public boolean hasNext() {
+            return false;
+        }
+        public E next() {
+            return null;
+        }
+    }
+}

regression/cbmc-java/lazyloading_indirect_generic_array_parameter/test.class

@@ -0,0 +1,11 @@
+public class ArrayListEquals {
+    
+    public int check2(ArrayList<Integer> l1) {
+        ArrayList<Integer> al = new ArrayList<Integer>();
+        if(l1.equals(al))
+            return 1;
+        else
+            return 0;
+    }
+
+}

regression/cbmc-java/lazyloading_indirect_generic_array_parameter/test.desc

@@ -0,0 +1,4 @@
+public interface Iterator<E> {
+    boolean hasNext();
+    E next();
+}

regression/cbmc-java/lazyloading_indirect_generic_array_parameter/test.java

@@ -0,0 +1,4 @@
+public interface List<E> {
+    ListIterator<E> listIterator();
+    ListIterator<E> listIterator(int index);
+}

regression/cbmc-java/lazyloading_multiple_generic_parameters/asserthere.class

@@ -0,0 +1,5 @@
+public interface ListIterator<E> extends Iterator<E> {
+    boolean hasNext();
+    boolean hasPrevious();
+    E next();
+}

regression/cbmc-java/lazyloading_multiple_generic_parameters/container.class

@@ -0,0 +1,6 @@
+CORE
+ArrayListEquals.class
+--lazy-methods --java-max-vla-length 48 --unwind 8 --java-unwind-enum-static --trace --cover location --function ArrayListEquals.check2 --show-goto-functions
+e2 . ArrayList\$Itr.hasNext:\(\)Z\(\);
+--
+e2 . ListIterator.hasNext:\(\)Z\(\);

regression/cbmc-java/lazyloading_multiple_generic_parameters/test.class

@@ -0,0 +1,5 @@
+public class Test {
+    public static void main(int x) {
+        assert(x == 0);
+    }
+}

regression/cbmc-java/lazyloading_multiple_generic_parameters/test.desc

@@ -0,0 +1,7 @@
+CORE
+Test.class
+--trace --json-ui --trace-json-extended
+^EXIT=10$
+^SIGNAL=0$
+rawLhs
+--

regression/cbmc-java/lazyloading_multiple_generic_parameters/test.java

@@ -0,0 +1,7 @@
+CORE
+Test.class
+--trace --json-ui
+^EXIT=10$
+^SIGNAL=0$
+--
+rawLhs

regression/cbmc-java/lazyloading_nested_generic_parameters/asserthere.class

@@ -0,0 +1,12 @@
+#include <stdint.h>
+#include <string.h>
+
+int main()
+{
+  uint8_t a;
+  uint32_t b;
+
+  memcpy(&b, &a, sizeof(b));
+
+  return 0;
+}

regression/cbmc-java/lazyloading_nested_generic_parameters/container.class

@@ -0,0 +1,10 @@
+CORE
+main.c
+--bounds-check --pointer-check
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+\[(__builtin___memcpy_chk|memcpy)\.pointer_dereference\.16\] dereference failure: pointer outside object bounds in \*\(\(\(const char \*\)src \+ \(signed long (long )?int\)n\) - \(signed long (long )?int\)1\): FAILURE$
+\*\* 1 of 17 failed
+--
+^warning: ignoring

regression/cbmc-java/lazyloading_nested_generic_parameters/container2.class

@@ -5,6 +5,6 @@ main.c
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
 \[.*] dereference failure: pointer outside dynamic object bounds in .*: FAILURE
-\*\* 1 of .* failed \(.*\)
+\*\* 2 of .* failed \(.*\)
 --
 ^warning: ignoring