Fixes setCause on default exception
authorJohn Toman <jtoman@cs.washington.edu>
Thu, 30 Aug 2018 20:58:26 +0000 (13:58 -0700)
committerJohn Toman <jtoman@cs.washington.edu>
Fri, 31 Aug 2018 19:41:24 +0000 (12:41 -0700)
src/classes/java/lang/Throwable.java
src/tests/gov/nasa/jpf/test/java/lang/ThrowableTest.java [new file with mode: 0644]

index ff19d97..719149c 100644 (file)
@@ -44,7 +44,7 @@ public class Throwable {
     } catch (ClassNotFoundException e) {
       throw new NoClassDefFoundError("java.lang.StackTraceElement");
     }
-     
+    cause = this;
     fillInStackTrace();
   }
 
diff --git a/src/tests/gov/nasa/jpf/test/java/lang/ThrowableTest.java b/src/tests/gov/nasa/jpf/test/java/lang/ThrowableTest.java
new file mode 100644 (file)
index 0000000..7ba19d7
--- /dev/null
@@ -0,0 +1,15 @@
+package gov.nasa.jpf.test.java.lang;
+
+import org.junit.Test;
+
+import gov.nasa.jpf.util.test.TestJPF;
+
+public class ThrowableTest extends TestJPF {
+  @Test
+  public void testSetCause() {
+    if(verifyNoPropertyViolation()) {
+      RuntimeException e = new RuntimeException();
+      e.initCause(new NullPointerException());
+    }
+  }
+}