Support Runtime.halt.

[jpf-core.git] / src / tests / gov / nasa / jpf / test / java / lang / RuntimeTest.java

diff --git a/src/tests/gov/nasa/jpf/test/java/lang/RuntimeTest.java b/src/tests/gov/nasa/jpf/test/java/lang/RuntimeTest.java
index e6e3d96b3cc3311d39d0b56ddf151ad4e72a6641..b03d28b12ecc8e14edc94d132b5838eb61a9674f 100644 (file)
--- a/src/tests/gov/nasa/jpf/test/java/lang/RuntimeTest.java
+++ b/src/tests/gov/nasa/jpf/test/java/lang/RuntimeTest.java
@@ -25,6 +25,22 @@ import org.junit.Test;
 
 public class RuntimeTest extends TestJPF {
 
+  @Test
+  public void testExit() {
+    if (verifyNoPropertyViolation()) {
+      System.exit(1);
+      assert(false);
+    }
+  }
+
+  @Test
+  public void testHalt() {
+    if (verifyNoPropertyViolation()) {
+      Runtime.getRuntime().halt(1);
+      assert(false);
+    }
+  }
+
   @Test
   public void testAvailableProcessors() {