Add regression test

Author: Matthias Güdemann

regression/cbmc-java/removed_virtual_functions/AbstractList$Itr.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/removed_virtual_functions/AbstractList.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/removed_virtual_functions/AbstractList.java

@@ -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/removed_virtual_functions/ArrayList$Itr.class

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

regression/cbmc-java/removed_virtual_functions/ArrayList$ListItr.class

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

regression/cbmc-java/removed_virtual_functions/ArrayList.class

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

regression/cbmc-java/removed_virtual_functions/ArrayList.java

@@ -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\(\);