From: Cyrille Artho <artho@kth.se>
Date: Fri, 23 Nov 2018 12:24:57 +0000 (+0100)
Subject: Fix for System.in.available().
X-Git-Url: http://plrg.eecs.uci.edu/git/?a=commitdiff_plain;h=55f4f09d392d1f721119ec3382caeffcefc9a895;p=jpf-core.git

Fix for System.in.available().
	modified:   src/classes/java/lang/System.java: Custom instance with fix.
	modified:   src/tests/gov/nasa/jpf/test/java/lang/SystemTest.java: Unit test.
---

diff --git a/src/classes/java/lang/System.java b/src/classes/java/lang/System.java
index e18ee64..72d613b 100644
--- a/src/classes/java/lang/System.java
+++ b/src/classes/java/lang/System.java
@@ -17,6 +17,7 @@
  */
 package java.lang;
 
+import java.io.BufferedInputStream;
 import java.io.InputStream;
 import java.io.PrintStream;
 import java.nio.channels.Channel;
@@ -34,7 +35,13 @@ public class System {
 
   static Properties properties;
 
-  public static InputStream in; // new BufferedInputStream(...);  // <2do> not yet
+  public static InputStream in = new InputStream() {
+    public int available() { return 0; }
+    public int read() { return -1; }
+    public int read(byte[] b, int off, int len) { return 0; }
+    public int read(byte[] b) { return 0; }
+  };
+
   public static PrintStream out;
   public static PrintStream err;
   
diff --git a/src/tests/gov/nasa/jpf/test/java/lang/SystemTest.java b/src/tests/gov/nasa/jpf/test/java/lang/SystemTest.java
index 836a169..da2deb1 100644
--- a/src/tests/gov/nasa/jpf/test/java/lang/SystemTest.java
+++ b/src/tests/gov/nasa/jpf/test/java/lang/SystemTest.java
@@ -20,6 +20,8 @@ package gov.nasa.jpf.test.java.lang;
 import gov.nasa.jpf.util.test.TestJPF;
 import gov.nasa.jpf.vm.Verify;
 
+import java.io.IOException;
+
 import org.junit.Test;
 
 /**
@@ -149,4 +151,15 @@ public class SystemTest extends TestJPF {
       }
     }
   }
+
+  @Test
+  public void testSystemIn() {
+    try {
+      if (verifyNoPropertyViolation()) {
+        assert(System.in.available() == 0);
+      }
+    } catch (IOException e) {
+      fail(e.getMessage());
+    }
+  }
 }