diff --git a/regression/jbmc-cover/remove-virtual-functions/MyHashMap$EntrySet.class b/regression/jbmc-cover/remove-virtual-functions/MyHashMap$EntrySet.class new file mode 100644 index 00000000000..f8dcad30c56 Binary files /dev/null and b/regression/jbmc-cover/remove-virtual-functions/MyHashMap$EntrySet.class differ diff --git a/regression/jbmc-cover/remove-virtual-functions/MyHashMap$KeySet.class b/regression/jbmc-cover/remove-virtual-functions/MyHashMap$KeySet.class new file mode 100644 index 00000000000..4ef4342a6bc Binary files /dev/null and b/regression/jbmc-cover/remove-virtual-functions/MyHashMap$KeySet.class differ diff --git a/regression/jbmc-cover/remove-virtual-functions/MyHashMap$UselessIterator.class b/regression/jbmc-cover/remove-virtual-functions/MyHashMap$UselessIterator.class new file mode 100644 index 00000000000..a413e546247 Binary files /dev/null and b/regression/jbmc-cover/remove-virtual-functions/MyHashMap$UselessIterator.class differ diff --git a/regression/jbmc-cover/remove-virtual-functions/MyHashMap.class b/regression/jbmc-cover/remove-virtual-functions/MyHashMap.class new file mode 100644 index 00000000000..dea0a5b7d65 Binary files /dev/null and b/regression/jbmc-cover/remove-virtual-functions/MyHashMap.class differ diff --git a/regression/jbmc-cover/remove-virtual-functions/MyHashMap.java b/regression/jbmc-cover/remove-virtual-functions/MyHashMap.java new file mode 100644 index 00000000000..3d69bc6859b --- /dev/null +++ b/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; + } + +} diff --git a/regression/jbmc-cover/remove-virtual-functions/MyIterator.class b/regression/jbmc-cover/remove-virtual-functions/MyIterator.class new file mode 100644 index 00000000000..ed2abe7d5fb Binary files /dev/null and b/regression/jbmc-cover/remove-virtual-functions/MyIterator.class differ diff --git a/regression/jbmc-cover/remove-virtual-functions/MyIterator.java b/regression/jbmc-cover/remove-virtual-functions/MyIterator.java new file mode 100644 index 00000000000..7b5caca0887 --- /dev/null +++ b/regression/jbmc-cover/remove-virtual-functions/MyIterator.java @@ -0,0 +1,7 @@ +public interface MyIterator { + + boolean someBoolean(); + + void next(); + +} diff --git a/regression/jbmc-cover/remove-virtual-functions/MySet.class b/regression/jbmc-cover/remove-virtual-functions/MySet.class new file mode 100644 index 00000000000..a2dc2f43c6d Binary files /dev/null and b/regression/jbmc-cover/remove-virtual-functions/MySet.class differ diff --git a/regression/jbmc-cover/remove-virtual-functions/MySet.java b/regression/jbmc-cover/remove-virtual-functions/MySet.java new file mode 100644 index 00000000000..a349d79a305 --- /dev/null +++ b/regression/jbmc-cover/remove-virtual-functions/MySet.java @@ -0,0 +1,5 @@ +public interface MySet { + + public MyIterator iterator(); + +} diff --git a/regression/jbmc-cover/remove-virtual-functions/test.desc b/regression/jbmc-cover/remove-virtual-functions/test.desc new file mode 100644 index 00000000000..49ff38dd402 --- /dev/null +++ b/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