diff --git a/src/java.base/share/classes/java/io/FileInputStream.java b/src/java.base/share/classes/java/io/FileInputStream.java index f206966a11ead..1429807070e98 100644 --- a/src/java.base/share/classes/java/io/FileInputStream.java +++ b/src/java.base/share/classes/java/io/FileInputStream.java @@ -31,6 +31,7 @@ import org.checkerframework.checker.index.qual.LTLengthOf; import org.checkerframework.checker.index.qual.NonNegative; import org.checkerframework.checker.mustcall.qual.MustCallAlias; +import org.checkerframework.dataflow.qual.SideEffectFree; import org.checkerframework.framework.qual.AnnotatedFor; import java.nio.channels.FileChannel; @@ -111,6 +112,7 @@ public class FileInputStream extends InputStream * to the file. * @see java.lang.SecurityManager#checkRead(java.lang.String) */ + @SideEffectFree public FileInputStream(String name) throws FileNotFoundException { this(name != null ? new File(name) : null); } @@ -142,6 +144,7 @@ public FileInputStream(String name) throws FileNotFoundException { * @see java.io.File#getPath() * @see java.lang.SecurityManager#checkRead(java.lang.String) */ + @SideEffectFree public FileInputStream(File file) throws FileNotFoundException { String name = (file != null ? file.getPath() : null); @SuppressWarnings("removal")