@@ -0,0 +1,1917 @@
+package de.fzi.cjunit.jpf.assumptions;%0A%0Aimport static org.hamcrest.MatcherAssert.assertThat;%0Aimport static org.hamcrest.Matchers.*;%0A%0Aimport java.util.List;%0A%0Aimport gov.nasa.jpf.Error;%0Aimport gov.nasa.jpf.jvm.NoUncaughtExceptionsProperty;%0A%0Aimport org.junit.Test;%0A%0Aimport de.fzi.cjunit.testutils.JPFForTesting;%0A%0A/*%0A * JPF provides its own implementation of some standard Java classes, but%0A * those implementations are in some cases incomplete, i.e. there are methods%0A * missing from the JPF implementation that are part of the public API or the%0A * originals.  This class collects some of those methods.%0A */%0Apublic class NoSuchMethodExceptionInJPF extends JPFForTesting %7B%0A%0A%09public static class GT %7B%0A%09%09public static void main(String%5B%5D args) %7B%0A%09%09%09assertThat(0, greaterThan(1));%0A%09%09%7D%0A%09%7D%0A%0A%09public static class GTOE %7B%0A%09%09public static void main(String%5B%5D args) %7B%0A%09%09%09assertThat(0, greaterThanOrEqualTo(1));%0A%09%09%7D%0A%09%7D%0A%0A%09public static class LT %7B%0A%09%09public static void main(String%5B%5D args) %7B%0A%09%09%09assertThat(1, lessThan(0));%0A%09%09%7D%0A%09%7D%0A%0A%09public static class LTOE %7B%0A%09%09public static void main(String%5B%5D args) %7B%0A%09%09%09assertThat(1, lessThanOrEqualTo(0));%0A%09%09%7D%0A%09%7D%0A%0A%09public void runTest(Class%3C?%3E app, Class%3C? extends Throwable%3E tc) %7B%0A%09%09createJPF(app);%0A%09%09NoUncaughtExceptionsProperty nuep%0A%09%09%09%09= new NoUncaughtExceptionsProperty(config);%0A%09%09jpf.addSearchProperty(nuep);%0A%09%09jpf.run();%0A%09%09List%3CError%3E errors = jpf.getSearchErrors();%0A%09%09assertThat(%22number of errors%22, errors.size(), equalTo(1));%0A%09%09assertThat(%22exception type%22,%0A%09%09%09%09nuep.getUncaughtExceptionInfo().getExceptionClassname(),%0A%09%09%09%09equalTo(tc.getName()));%0A%09%7D%0A%0A%09@Test%0A%09public void testGT() %7B%0A%09%09runTest(GT.class, AssertionError.class);%0A%09%7D%0A%0A%09@Test%0A%09public void testGTOE() %7B%0A%09%09runTest(GTOE.class, NoSuchMethodException.class);%0A%09%7D%0A%0A%09@Test%0A%09public void testLT() %7B%0A%09%09runTest(LT.class, NoSuchMethodException.class);%0A%09%7D%0A%0A%09@Test%0A%09public void testLTOE() %7B%0A%09%09runTest(LTOE.class, NoSuchMethodException.class);%0A%09%7D%0A%7D%0A

Add test to show "surprising" NoSuchMethodExceptions in JPF