Fix for System.in.available().
authorCyrille Artho <artho@kth.se>
Fri, 23 Nov 2018 12:24:57 +0000 (13:24 +0100)
committerCyrille Artho <artho@kth.se>
Fri, 23 Nov 2018 12:24:57 +0000 (13:24 +0100)
modified:   src/classes/java/lang/System.java: Custom instance with fix.
modified:   src/tests/gov/nasa/jpf/test/java/lang/SystemTest.java: Unit test.

src/classes/java/lang/System.java
src/tests/gov/nasa/jpf/test/java/lang/SystemTest.java

index e18ee640f8be74502db20e02bf24d05b14d16acf..72d613b4980ec8aabcaabef90e84c41209799946 100644 (file)
@@ -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;
   
index 836a16944cbae643fe19b36cdf7d106d5f8a4bf2..da2deb17710da58f328539da0025652925e2081b 100644 (file)
@@ -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());
+    }
+  }
 }