From: Dan Smith Date: Thu, 17 May 2018 06:15:26 +0000 (-0700) Subject: Fix incorrect IncompatibleClassChangeError in ClassInfo.getDefaultMethod (#7) X-Git-Url: http://plrg.eecs.uci.edu/git/?p=jpf-core.git;a=commitdiff_plain;h=18a0c42de3e80be0c2ddcf0d212e376e576fcda0;ds=sidebyside Fix incorrect IncompatibleClassChangeError in ClassInfo.getDefaultMethod (#7) The logic to detect if there are two conflicting default methods was incorrect. If a class and its superclass both implement the same interface JPF should not throw an IncompatibleClassChangeError. --- diff --git a/src/main/gov/nasa/jpf/vm/ClassInfo.java b/src/main/gov/nasa/jpf/vm/ClassInfo.java index d26abed..d9e5331 100644 --- a/src/main/gov/nasa/jpf/vm/ClassInfo.java +++ b/src/main/gov/nasa/jpf/vm/ClassInfo.java @@ -1095,7 +1095,7 @@ public class ClassInfo extends InfoObject implements Iterable, Gener for (ClassInfo ciIfc : ci.interfaces){ MethodInfo miIfc = ciIfc.getMethod(uniqueName, true); if (miIfc != null && !miIfc.isAbstract()){ - if (mi != null){ + if (mi != null && !mi.equals(miIfc)){ // this has to throw a IncompatibleClassChangeError in the client since Java prohibits ambiguous default methods String msg = "Conflicting default methods: " + mi.getFullName() + ", " + miIfc.getFullName(); throw new ClassChangeException(msg); diff --git a/src/tests/gov/nasa/jpf/test/vm/basic/MethodTest.java b/src/tests/gov/nasa/jpf/test/vm/basic/MethodTest.java index 76e114e..24a05ae 100644 --- a/src/tests/gov/nasa/jpf/test/vm/basic/MethodTest.java +++ b/src/tests/gov/nasa/jpf/test/vm/basic/MethodTest.java @@ -255,4 +255,24 @@ public class MethodTest extends TestMethodBase { assert a.foo() == 1 : "wrong A.foo() called for A1"; } } + + + interface InterfaceWithDefaultMethod { + default int foo() { + return 42; + } + } + + static class Base implements InterfaceWithDefaultMethod { + } + + static class Child extends Base implements InterfaceWithDefaultMethod { + } + + @Test + public void testDefaultMethodCall() { + if (verifyNoPropertyViolation()) { + assertEquals(42, new Child().foo()); + } + } }