From: John Toman <jtoman@cs.washington.edu>
Date: Thu, 30 Aug 2018 20:58:26 +0000 (-0700)
Subject: Fixes setCause on default exception
X-Git-Url: http://plrg.eecs.uci.edu/git/?a=commitdiff_plain;h=47dc4e2186cef79587b67fd5ca28188b97e73ce9;p=jpf-core.git

Fixes setCause on default exception
---

diff --git a/src/classes/java/lang/Throwable.java b/src/classes/java/lang/Throwable.java
index ff19d97..719149c 100644
--- a/src/classes/java/lang/Throwable.java
+++ b/src/classes/java/lang/Throwable.java
@@ -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
index 0000000..7ba19d7
--- /dev/null
+++ b/src/tests/gov/nasa/jpf/test/java/lang/ThrowableTest.java
@@ -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());
+    }
+  }
+}