Merge pull request #1239 from reuk/virtual-function-unwinding

Add test showing infinite unwinding

Author: peterschrammel

regression/cbmc-java/virtual_function_unwinding/Inner.class

@@ -0,0 +1,19 @@
+interface Interface {
+  boolean b();
+}
+
+class Inner implements Interface {
+  public boolean b() { return false; }
+}
+
+class Outer implements Interface {
+  private Interface inner;
+  public Outer(Interface inner) { this.inner = inner; }
+  public boolean b() { return !inner.b(); }
+}
+
+public class Virtual {
+  public static void main(String[] args) {
+    assert new Outer(new Inner()).b();
+  }
+}

regression/cbmc-java/virtual_function_unwinding/Interface.class

@@ -0,0 +1,8 @@
+KNOWNBUG
+Virtual.class
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+See diffblue/test-gen#845 for details