Regression test for remove_virtual_functions [TG-1404]

regression/jbmc-cover/remove-virtual-functions/MyHashMap.java

@@ -0,0 +1,60 @@
+import java.io.PrintStream;
+
+public class MyHashMap {
+
+    private Integer[] table;
+    private int size;
+
+    public MyHashMap() {
+        table = new Integer[8];
+        size = 0;
+    }
+
+    public void put(Integer key) {
+        table[size++] = key;
+    }
+
+    public MySet entrySet() {
+        return new EntrySet();
+    }
+
+    class EntrySet implements MySet {
+        public final MyIterator iterator() {
+            return new UselessIterator();
+        }
+    }
+
+    class UselessIterator implements MyIterator {
+        boolean b;
+        UselessIterator() {
+            b = true;
+        }
+        public boolean someBoolean() {
+            return b;
+        }
+        public void next() {
+            b = false;
+        }
+    }
+
+    public MySet keySet() {
+        return new KeySet();
+    }
+
+    class KeySet implements MySet {
+        public final MyIterator iterator() {
+            return new UselessIterator();
+        }
+    }
+
+    public static boolean test() {
+        MyHashMap hm = new MyHashMap();
+        MySet es = hm.entrySet();
+        MyIterator it = es.iterator();
+        while (it.someBoolean()) {
+            it.next();
+        }
+        return true;
+    }
+
+}

regression/jbmc-cover/remove-virtual-functions/MyIterator.java

@@ -0,0 +1,7 @@
+public interface MyIterator {
+
+    boolean someBoolean();
+
+    void next();
+
+}

regression/jbmc-cover/remove-virtual-functions/MySet.java

@@ -0,0 +1,5 @@
+public interface MySet {
+
+    public MyIterator iterator();
+
+}

regression/jbmc-cover/remove-virtual-functions/test.desc

@@ -0,0 +1,8 @@
+CORE
+MyHashMap.class
+--function MyHashMap.test --unwind 5 --cover location
+java::MyHashMap.test.*coverage.*SATISFIED
+--
+java::MyHashMap.test.*coverage.*FAILED
+--
+Checks that TG-1404 is fixed