Merge pull request #1666 from mgudemann/bugfix/removed_required_virtual_calls

[TG-1523] fix removed required virtual calls

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;
+    }
+
+}