Annotate java.util.zip.

Prompted by
google/xplat@4461165.

Author: cpovirk

src/java.base/share/classes/java/util/zip/Adler32.java

@@ -30,6 +30,7 @@
 import jdk.internal.util.Preconditions;
 import jdk.internal.vm.annotation.IntrinsicCandidate;
 import sun.nio.ch.DirectBuffer;
+import org.jspecify.annotations.NullMarked;
 
 import static java.util.zip.ZipUtils.NIO_ACCESS;
 
@@ -44,6 +45,7 @@
  * @author      David Connelly
  * @since 1.1
  */
+@NullMarked
 public class Adler32 implements Checksum {
 
     private int adler = 1;

src/java.base/share/classes/java/util/zip/Checksum.java

@@ -28,14 +28,15 @@
 import org.checkerframework.framework.qual.AnnotatedFor;
 
 import java.nio.ByteBuffer;
+import org.jspecify.annotations.NullMarked;
 
 /**
  * An interface representing a data checksum.
  *
  * @author David Connelly
  * @since 1.1
  */
-@AnnotatedFor({"index"})
+@NullMarked
 public interface Checksum {
 
     /**
@@ -69,7 +70,7 @@ default public void update(byte[] b) {
      * @param off the start offset of the data
      * @param len the number of bytes to use for the update
      */
-    public void update(byte[] b, @IndexOrHigh({"#1"}) int off, @IndexOrHigh({"#1"}) int len);
+    public void update(byte[] b, int off, int len);
 
     /**
      * Updates the current checksum with the bytes from the specified buffer.

src/java.base/share/classes/java/util/zip/DataFormatException.java

@@ -25,12 +25,16 @@
 
 package java.util.zip;
 
+import org.jspecify.annotations.NullMarked;
+import org.jspecify.annotations.Nullable;
+
 /**
  * Signals that a data format error has occurred.
  *
  * @author      David Connelly
  * @since 1.1
  */
+@NullMarked
 public class DataFormatException extends Exception {
     @java.io.Serial
     private static final long serialVersionUID = 2219632870893641452L;
@@ -47,7 +51,7 @@ public DataFormatException() {
      * A detail message is a String that describes this particular exception.
      * @param s the String containing a detail message
      */
-    public DataFormatException(String s) {
+    public DataFormatException(@Nullable String s) {
         super(s);
     }
 }

src/java.base/share/classes/java/util/zip/Deflater.java

@@ -33,6 +33,7 @@
 import jdk.internal.ref.CleanerFactory;
 import jdk.internal.util.Preconditions;
 import sun.nio.ch.DirectBuffer;
+import org.jspecify.annotations.NullMarked;
 
 import static java.util.zip.ZipUtils.NIO_ACCESS;
 
@@ -70,7 +71,7 @@
  * @author      David Connelly
  * @since 1.1
  */
-
+@NullMarked
 public class Deflater {
 
     private final DeflaterZStreamRef zsRef;

src/java.base/share/classes/java/util/zip/DeflaterOutputStream.java

@@ -29,6 +29,7 @@
 import java.io.OutputStream;
 import java.io.InputStream;
 import java.io.IOException;
+import org.jspecify.annotations.NullMarked;
 
 /**
  * This class implements an output stream filter for compressing data in
@@ -42,6 +43,7 @@
  * @author      David Connelly
  * @since 1.1
  */
+@NullMarked
 public class DeflaterOutputStream extends FilterOutputStream {
     /**
      * Compressor for this stream.

src/java.base/share/classes/java/util/zip/Inflater.java

@@ -33,6 +33,7 @@
 import jdk.internal.ref.CleanerFactory;
 import jdk.internal.util.Preconditions;
 import sun.nio.ch.DirectBuffer;
+import org.jspecify.annotations.NullMarked;
 
 import static java.util.zip.ZipUtils.NIO_ACCESS;
 
@@ -70,7 +71,7 @@
  * @since 1.1
  *
  */
-
+@NullMarked
 public class Inflater {
 
     private final InflaterZStreamRef zsRef;

src/java.base/share/classes/java/util/zip/InflaterOutputStream.java

@@ -25,15 +25,11 @@
 
 package java.util.zip;
 
-import org.checkerframework.checker.index.qual.IndexOrHigh;
-import org.checkerframework.checker.index.qual.Positive;
-import org.checkerframework.checker.signedness.qual.PolySigned;
-import org.checkerframework.framework.qual.AnnotatedFor;
-
 import java.io.FilterOutputStream;
 import java.io.IOException;
 import java.io.OutputStream;
 import java.util.Objects;
+import org.jspecify.annotations.NullMarked;
 
 /**
  * Implements an output stream filter for uncompressing data stored in the
@@ -46,8 +42,7 @@
  * @see DeflaterInputStream
  * @see DeflaterOutputStream
  */
-
-@AnnotatedFor({"index", "signedness"})
+@NullMarked
 public class InflaterOutputStream extends FilterOutputStream {
     /** Decompressor for this stream. */
     protected final Inflater inf;
@@ -107,7 +102,7 @@ public InflaterOutputStream(OutputStream out, Inflater infl) {
      * @throws IllegalArgumentException if {@code bufLen <= 0}
      * @throws NullPointerException if {@code out} or {@code infl} is null
      */
-    public InflaterOutputStream(OutputStream out, Inflater infl, @Positive int bufLen) {
+    public InflaterOutputStream(OutputStream out, Inflater infl, int bufLen) {
         super(out);
 
         // Sanity checks
@@ -225,7 +220,7 @@ public void write(int b) throws IOException {
      * @throws NullPointerException if {@code b} is null
      * @throws ZipException if a compression (ZIP) format error occurs
      */
-    public void write(@PolySigned byte[] b, @IndexOrHigh({"#1"}) int off, @IndexOrHigh({"#1"}) int len) throws IOException {
+    public void write(byte[] b, int off, int len) throws IOException {
         // Sanity checks
         ensureOpen();
         if (b == null) {

src/java.base/share/classes/java/util/zip/ZipException.java

@@ -26,14 +26,16 @@
 package java.util.zip;
 
 import java.io.IOException;
+import org.jspecify.annotations.NullMarked;
+import org.jspecify.annotations.Nullable;
 
 /**
  * Signals that a ZIP exception of some sort has occurred.
  *
  * @see     java.io.IOException
  * @since   1.1
  */
-
+@NullMarked
 public class ZipException extends IOException {
     @java.io.Serial
     private static final long serialVersionUID = 8000196834066748623L;
@@ -53,7 +55,7 @@ public ZipException() {
      * @param   s   the detail message.
      */
 
-    public ZipException(String s) {
+    public ZipException(@Nullable String s) {
         super(s);
     }
 }