diff --git a/__test__ b/__test__ new file mode 100644 index 00000000..93a52737 --- /dev/null +++ b/__test__ @@ -0,0 +1 @@ +*** \ No newline at end of file diff --git a/_test_ b/_test_ new file mode 100644 index 00000000..e69de29b diff --git a/lib/junit-4.13.2.jar b/lib/junit-4.13.2.jar new file mode 100644 index 00000000..6da55d8b Binary files /dev/null and b/lib/junit-4.13.2.jar differ diff --git a/src/main/gov/nasa/jpf/D.java b/src/main/gov/nasa/jpf/D.java new file mode 100644 index 00000000..c85e3643 --- /dev/null +++ b/src/main/gov/nasa/jpf/D.java @@ -0,0 +1,8 @@ +package gov.nasa.jpf; + +public class D { + // Non-static method + public void m() { + System.out.println("Non-static method executed."); + } +} diff --git a/src/tests/gov/nasa/jpf/StaticCallToNonStaticTest.java b/src/tests/gov/nasa/jpf/StaticCallToNonStaticTest.java index 323eb4c9..05752299 100644 --- a/src/tests/gov/nasa/jpf/StaticCallToNonStaticTest.java +++ b/src/tests/gov/nasa/jpf/StaticCallToNonStaticTest.java @@ -5,23 +5,15 @@ public class StaticCallToNonStaticTest extends TestJPF { - // A non-static method - public void nonStaticMethod() { - System.out.println("Non-static method executed."); - } - - // Test case to verify JPF behavior @Test public void testStaticCallToNonStatic() { - // Using JPF’s verification mechanism if (verifyNoPropertyViolation()) { - // Simulating a static method call to a non-static method - StaticCallToNonStaticTest instance = null; try { - instance.nonStaticMethod(); // This should fail because it's a static call to a non-static method - } catch (NullPointerException e) { - // Expected exception: this will be caught as instance is null - System.out.println("Caught expected NullPointerException: " + e.getMessage()); + // Attempting to call non-static method m() on class D without an instance + D.m(); // This should throw IncompatibleClassChangeError after D.java is recompiled without static + } catch (IncompatibleClassChangeError e) { + // Expected exception: this is the behavior we want to test + System.out.println("Caught expected IncompatibleClassChangeError: " + e.getMessage()); } } }