more robust: file length can be invalid in odd situations;
authorwenzelm
Sat, 23 Nov 2019 11:28:15 +0100
changeset 71152 f2d848a596d1
parent 71151 69a22ccd1817
child 71153 8563046f15c3
more robust: file length can be invalid in odd situations;
src/Pure/General/bytes.scala
--- a/src/Pure/General/bytes.scala	Sat Nov 23 11:19:18 2019 +0100
+++ b/src/Pure/General/bytes.scala	Sat Nov 23 11:28:15 2019 +0100
@@ -66,7 +66,11 @@
     }
 
   def read(file: JFile): Bytes =
-    using(new FileInputStream(file))(read_stream(_, limit = file.length.toInt))
+  {
+    val length = file.length
+    val limit = if (length < 0 || length > Integer.MAX_VALUE) Integer.MAX_VALUE else length.toInt
+    using(new FileInputStream(file))(read_stream(_, limit = limit))
+  }
 
   def read(path: Path): Bytes = read(path.file)