Fixes setCause on default exception

diff --git a/src/classes/java/lang/Throwable.java b/src/classes/java/lang/Throwable.java
index ff19d976bf128d3762f35651c3372c57b9e4733e..719149cf91f482d386ea677781ff3869780cf2ef 100644 (file)
--- 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 (file)
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());
+    }
+  }
+}