Annotations for CSV version 1.9.0

Author: mernst

.gitignore

@@ -14,6 +14,7 @@ buildNumber.properties
 # https://github.com/takari/maven-wrapper#usage-without-binary-jar
 .mvn/wrapper/maven-wrapper.jar
 
+
 .classpath
 .project
 .settings/

pom.xml

@@ -312,7 +312,6 @@
           </annotationProcessors>
           <compilerArgs>
             <arg>-J-Xbootclasspath/p:${errorProneJavac}</arg>
-            <arg>-Xbootclasspath/p:${annotatedJdk}</arg>
             <!-- -Awarns turns type-checking warnings into errors. -->
             <!-- <arg>-Awarns</arg> -->
           </compilerArgs>
@@ -649,7 +648,6 @@
             <configuration>
               <fork>true</fork>
               <compilerArgs combine.children="append">
-                <arg>-Xbootclasspath/p:${annotatedJdk}</arg>
                 <arg>-J-Xbootclasspath/p:${settings.localRepository}/com/google/errorprone/javac/${javac.version}/javac-${javac.version}.jar</arg>
               </compilerArgs>
             </configuration>

src/main/java/org/apache/commons/csv/CSVFormat.java

@@ -17,6 +17,7 @@
 
 package org.apache.commons.csv;
 
+import org.checkerframework.checker.nullness.qual.PolyNull;
 import org.checkerframework.checker.initialization.qual.UnknownInitialization;
 import org.checkerframework.checker.nullness.qual.AssertNonNullIfNonNull;
 import org.checkerframework.checker.nullness.qual.EnsuresNonNullIf;
@@ -203,31 +204,31 @@ public static Builder create(final CSVFormat csvFormat) {
 
         private boolean autoFlush;
 
-        private Character commentMarker;
+        private @Nullable Character commentMarker;
 
         private String delimiter;
 
-        private Character escapeCharacter;
+        private @Nullable Character escapeCharacter;
 
-        private String[] headerComments;
+        private @Nullable String @Nullable [] headerComments;
 
-        private String[] headers;
+        private String @Nullable[] headers;
 
         private boolean ignoreEmptyLines;
 
         private boolean ignoreHeaderCase;
 
         private boolean ignoreSurroundingSpaces;
 
-        private String nullString;
+        private @Nullable String nullString;
 
-        private Character quoteCharacter;
+        private @Nullable Character quoteCharacter;
 
         private String quotedNullString;
 
-        private QuoteMode quoteMode;
+        private @Nullable QuoteMode quoteMode;
 
-        private String recordSeparator;
+        private @Nullable String recordSeparator;
 
         private boolean skipHeaderRecord;
 
@@ -324,7 +325,7 @@ public Builder setCommentMarker(final char commentMarker) {
          * @return This instance.
          * @throws IllegalArgumentException thrown if the specified character is a line break
          */
-        public Builder setCommentMarker(final Character commentMarker) {
+        public Builder setCommentMarker(final @Nullable Character commentMarker) {
             if (isLineBreak(commentMarker)) {
                 throw new IllegalArgumentException("The comment start marker character cannot be a line break");
             }
@@ -375,7 +376,7 @@ public Builder setEscape(final char escapeCharacter) {
          * @return This instance.
          * @throws IllegalArgumentException thrown if the specified character is a line break
          */
-        public Builder setEscape(final Character escapeCharacter) {
+        public Builder setEscape(final @Nullable Character escapeCharacter) {
             if (isLineBreak(escapeCharacter)) {
                 throw new IllegalArgumentException("The escape character cannot be a line break");
             }
@@ -404,10 +405,11 @@ public Builder setEscape(final Character escapeCharacter) {
          * @param headerEnum the enum defining the header, {@code null} if disabled, empty if parsed automatically, user specified otherwise.
          * @return This instance.
          */
-        public Builder setHeader(final Class<? extends Enum<?>> headerEnum) {
+        public Builder setHeader(final @Nullable Class<? extends Enum<?>> headerEnum) {
             String[] header = null;
             if (headerEnum != null) {
-                final Enum<?>[] enumValues = headerEnum.getEnumConstants();
+                @SuppressWarnings({"dereference.of.nullable", "assignment"})  // headerEnum is an enum, so getEnumConstants is non-null
+                final Enum<?> @NonNull [] enumValues = headerEnum.getEnumConstants();
                 header = new String[enumValues.length];
                 for (int i = 0; i < enumValues.length; i++) {
                     header[i] = enumValues[i].name();
@@ -436,7 +438,7 @@ public Builder setHeader(final Class<? extends Enum<?>> headerEnum) {
          * @return This instance.
          * @throws SQLException SQLException if a database access error occurs or this method is called on a closed result set.
          */
-        public Builder setHeader(final ResultSet resultSet) throws SQLException {
+        public Builder setHeader(final @Nullable ResultSet resultSet) throws SQLException {
             return setHeader(resultSet != null ? resultSet.getMetaData() : null);
         }
 
@@ -460,7 +462,7 @@ public Builder setHeader(final ResultSet resultSet) throws SQLException {
          * @return This instance.
          * @throws SQLException SQLException if a database access error occurs or this method is called on a closed result set.
          */
-        public Builder setHeader(final ResultSetMetaData resultSetMetaData) throws SQLException {
+        public Builder setHeader(final @Nullable ResultSetMetaData resultSetMetaData) throws SQLException {
             String[] labels = null;
             if (resultSetMetaData != null) {
                 final int columnCount = resultSetMetaData.getColumnCount();
@@ -491,7 +493,7 @@ public Builder setHeader(final ResultSetMetaData resultSetMetaData) throws SQLEx
          * @param header the header, {@code null} if disabled, empty if parsed automatically, user specified otherwise.
          * @return This instance.
          */
-        public Builder setHeader(final String... header) {
+        public Builder setHeader(final String @Nullable ... header) {
             this.headers = CSVFormat.clone(header);
             return this;
         }
@@ -506,7 +508,7 @@ public Builder setHeader(final String... header) {
          * @param headerComments the headerComments which will be printed by the Printer before the actual CSV data.
          * @return This instance.
          */
-        public Builder setHeaderComments(final Object... headerComments) {
+        public Builder setHeaderComments(final @Nullable Object @Nullable ... headerComments) {
             this.headerComments = CSVFormat.clone(toStringArray(headerComments));
             return this;
         }
@@ -521,7 +523,7 @@ public Builder setHeaderComments(final Object... headerComments) {
          * @param headerComments the headerComments which will be printed by the Printer before the actual CSV data.
          * @return This instance.
          */
-        public Builder setHeaderComments(final String... headerComments) {
+        public Builder setHeaderComments(final @Nullable String @Nullable ... headerComments) {
             this.headerComments = CSVFormat.clone(headerComments);
             return this;
         }
@@ -572,7 +574,7 @@ public Builder setIgnoreSurroundingSpaces(final boolean ignoreSurroundingSpaces)
          * @param nullString the String to convert to and from {@code null}. No substitution occurs if {@code null}.
          * @return This instance.
          */
-        public Builder setNullString(final String nullString) {
+        public Builder setNullString(final @Nullable String nullString) {
             this.nullString = nullString;
             this.quotedNullString = quoteCharacter + nullString + quoteCharacter;
             return this;
@@ -595,7 +597,7 @@ public Builder setQuote(final char quoteCharacter) {
          * @param quoteCharacter the quote character, use {@code null} to disable.
          * @return This instance.
          */
-        public Builder setQuote(final Character quoteCharacter) {
+        public Builder setQuote(final @Nullable Character quoteCharacter) {
             if (isLineBreak(quoteCharacter)) {
                 throw new IllegalArgumentException("The quoteChar cannot be a line break");
             }
@@ -1161,7 +1163,7 @@ public CSVFormat getFormat() {
      * @return the cloned array.
      */
     @SafeVarargs
-    static <T> T[] clone(final T... values) {
+    static <T> T @PolyNull [] clone(final T @PolyNull ... values) {
         return values == null ? null : values.clone();
     }
 
@@ -1231,7 +1233,8 @@ public static CSVFormat newFormat(final char delimiter) {
                 true);
     }
 
-    private @Nullable String @Nullable [] toStringArray(@UnknownInitialization(java.lang.Object.class) @NonNull CSVFormat this, final @Nullable Object @Nullable [] values) {
+    @SuppressWarnings("nullness:argument")  // Objects.toString(..., ...) needs @PolyNull (has it after CF 3.17.0)
+    static @Nullable String @PolyNull [] toStringArray(final @Nullable Object @PolyNull [] values) {
         if (values == null) {
             return null;
         }
@@ -1284,7 +1287,7 @@ public static CSVFormat valueOf(final String format) {
 
     private final String @MonotonicNonNull [] header; // array of header column names
 
-    private final @Nullable String @MonotonicNonNull [] headerComments; // array of header comment lines
+    private final @Nullable String @Nullable [] headerComments; // array of header comment lines
 
     private final boolean ignoreEmptyLines;
 
@@ -1353,7 +1356,7 @@ private CSVFormat(final Builder builder) {
      * @param autoFlush               TODO Doc me.
      * @throws IllegalArgumentException if the delimiter is a line break character.
      */
-    @SuppressWarnings("nullness:assignment.type.incompatible") // initializing @MonotonicNonNull: https://github.com/typetools/checker-framework/issues/2215
+    @SuppressWarnings("nullness:assignment") // initializing @MonotonicNonNull: https://github.com/typetools/checker-framework/issues/2215
     private CSVFormat(final String delimiter, final @Nullable Character quoteChar, final @Nullable QuoteMode quoteMode,
             final @Nullable Character commentStart, final @Nullable Character escape, final boolean ignoreSurroundingSpaces,
             final boolean ignoreEmptyLines, final @Nullable String recordSeparator, final @Nullable String nullString,
@@ -1514,6 +1517,7 @@ public char getDelimiter() {
      *
      * @return the delimiter.
      */
+    @Pure
     public String getDelimiterString() {
         return delimiter;
     }
@@ -1547,7 +1551,7 @@ public String getDelimiterString() {
     @AssertNonNullIfNonNull("headerComments")
     @Pure // not actually pure, but pure up to .equals, and this suppresses a warning elsewhere
     @SuppressWarnings("nullness") // return @MonotonicNonNull field: https://github.com/typetools/checker-framework/issues/2216
-    public @Nullable String @MonotonicNonNull [] getHeaderComments() {
+    public @Nullable String @Nullable [] getHeaderComments() {
         return headerComments != null ? headerComments.clone() : null;
     }
 
@@ -1873,7 +1877,7 @@ public CSVPrinter print(final Path out, final Charset charset) throws IOExceptio
         return print(Files.newBufferedWriter(out, charset));
     }
 
-    @SuppressWarnings("contracts.precondition.not.satisfied") // Maybe a bug in commmons-csv:
+    @SuppressWarnings("contracts.precondition") // Maybe a bug in commmons-csv:
     // if quoteCharacter==NONE and isEscapeCharacterSet()==false, an exception is thrown.
     private void print(final Reader reader, final Appendable out, final boolean newRecord) throws IOException {
         // Reader is never null
@@ -2588,7 +2592,7 @@ public CSVFormat withHeader(final String @Nullable ... header) {
      * @deprecated Use {@link Builder#setHeaderComments(Object...)}
      */
     @Deprecated
-    public CSVFormat withHeaderComments(final Object... headerComments) {
+    public CSVFormat withHeaderComments(final @Nullable Object @Nullable ... headerComments) {
         return builder().setHeaderComments(headerComments).build();
     }
 

src/main/java/org/apache/commons/csv/CSVParser.java

@@ -148,7 +148,7 @@ public final class CSVParser implements Iterable<CSVRecord>, Closeable {
     class CSVRecordIterator implements Iterator<CSVRecord> {
         private @Nullable CSVRecord current;
 
-        @SuppressWarnings("contracts.precondition.not.satisfied")  // TODO: how to express @RequiresNonNull({"CSVParser.this.format"})
+        // @SuppressWarnings("contracts.precondition")  // TODO: how to express @RequiresNonNull({"CSVParser.this.format"})
         private @Nullable CSVRecord getNextRecord() {
             try {
                 return CSVParser.this.nextRecord();
@@ -437,13 +437,14 @@ public CSVParser(final Reader reader, final CSVFormat format, final long charact
         this.format = format.copy();
         this.lexer = new Lexer(format, new ExtendedBufferedReader(reader));
         this.csvRecordIterator = new CSVRecordIterator();
-        this.headers = createHeaders();
+        @SuppressWarnings("method.invocation")  // receiver is not yet initialized; likely bug; see comment at createHeaders.
+        Headers _headers = createHeaders();
+        this.headers = _headers;
         this.characterOffset = characterOffset;
         this.recordNumber = recordNumber - 1;
     }
 
-    @RequiresNonNull("format")
-    private void addRecordValue(@UnknownInitialization(Object.class) CSVParser this, final boolean lastRecord) {
+    private void addRecordValue(final boolean lastRecord) {
         final String input = this.reusableToken.content.toString();
         final String inputClean = this.format.getTrim() ? input.trim() : input;
         if (lastRecord && inputClean.isEmpty() && this.format.getTrailingDelimiter()) {
@@ -478,8 +479,8 @@ private Map<String, Integer> createEmptyHeaderMap(@UnknownInitialization(Object.
      * @return null if the format has no header.
      * @throws IOException if there is a problem reading the header or skipping the first record
      */
-    @RequiresNonNull({"format", "lexer"})
-    private Headers createHeaders(@UnknownInitialization(Object.class) CSVParser this) throws IOException {
+    // Possible bug in commons-csv: This is called from the constructor, when characterOffset and recordNumber are not yet set.  This method calls nextRecord(), which reads characterOffset.
+    private Headers createHeaders() throws IOException {
         Map<String, Integer> hdrMap = null;
         List<String> headerNames = null;
         final String[] formatHeader = this.format.getHeader();
@@ -648,7 +649,7 @@ public List<CSVRecord> getRecords() throws IOException {
      *           the cell data to further processed
      * @return null if input is parsed as null, or input itself if input isn't parsed as null
      */
-    private String handleNull(final String input) {
+    private @Nullable String handleNull(final String input) {
         final boolean isQuoted = this.reusableToken.isQuoted;
         final String nullString = format.getNullString();
         final boolean strictQuoteMode = isStrictQuoteMode();
@@ -704,8 +705,7 @@ public Iterator<CSVRecord> iterator() {
      * @throws IOException
      *             on parse error or input read-failure
      */
-    @RequiresNonNull({"lexer", "format"})
-    @Nullable CSVRecord nextRecord(@UnknownInitialization(Object.class) CSVParser this) throws IOException {
+    @Nullable CSVRecord nextRecord() throws IOException {
         CSVRecord result = null;
         this.recordList.clear();
         StringBuilder sb = null;

src/main/java/org/apache/commons/csv/CSVPrinter.java

@@ -191,7 +191,7 @@ public void print(final @Nullable Object value) throws IOException {
      *             If an I/O error occurs
      */
     @SuppressWarnings("nullness") // getCommentMarker() isn't affected by side effects in this method
-    public void printComment(final String comment) throws IOException {
+    public void printComment(final @Nullable String comment) throws IOException {
         if (comment == null || !format.isCommentMarkerSet()) {
             return;
         }
@@ -229,6 +229,7 @@ public void printComment(final String comment) throws IOException {
      * @throws SQLException If a database access error occurs or this method is called on a closed result set.
      * @since 1.9.0
      */
+    @SuppressWarnings("nullness:argument")  // getHeader() returns non-null because setHeader() was called on non-null
     public void printHeaders(final ResultSet resultSet) throws IOException, SQLException {
         printRecord((Object[]) format.builder().setHeader(resultSet).build().getHeader());
     }

src/main/java/org/apache/commons/csv/CSVRecord.java

@@ -227,6 +227,7 @@ public boolean isConsistent() {
      *            the name of the column to be retrieved.
      * @return whether a given column is mapped.
      */
+    @SuppressWarnings({"expression.unparsable", "flowexpr.parse.error", "contracts.conditional.postcondition"})  // https://github.com/typetools/checker-framework/issues/4858
     @EnsuresKeyForIf(expression="#1", map="getHeaderMapRaw()", result=true)
     @EnsuresNonNullIf(expression="getHeaderMapRaw()", result=true)
     public boolean isMapped(final String name) {
@@ -253,6 +254,7 @@ public boolean isSet(final int index) {
      *            the name of the column to be retrieved.
      * @return whether a given columns is mapped and has a value
      */
+    @SuppressWarnings({"expression.unparsable", "flowexpr.parse.error.postcondition", "dereference.of.nullable"})  // https://github.com/typetools/checker-framework/issues/4858
     public boolean isSet(final String name) {
         return isMapped(name) && getHeaderMapRaw().get(name).intValue() < values.length;
     }
@@ -275,6 +277,7 @@ public boolean isSet(final String name) {
      * @return the given map.
      * @since 1.9.0
      */
+    @SuppressWarnings({"lambda.param", "expression.unparsable"})  // https://github.com/typetools/checker-framework/issues/4858
     public <M extends Map<String, @Nullable String>> M putIn(final M map) {
         if (getHeaderMapRaw() == null) {
             return map;
@@ -303,7 +306,7 @@ public int size() {
      * @return the new stream.
      * @since 1.9.0
      */
-    public Stream<String> stream() {
+    public Stream<@Nullable String> stream() {
         return Stream.of(values);
     }
 

src/main/java/org/apache/commons/csv/Lexer.java

@@ -17,8 +17,10 @@
 
 package org.apache.commons.csv;
 
+import org.checkerframework.checker.initialization.qual.UnknownInitialization;
 import org.checkerframework.checker.nullness.qual.Nullable;
 import org.checkerframework.checker.nullness.qual.MonotonicNonNull;
+
 import static org.apache.commons.csv.Constants.BACKSPACE;
 import static org.apache.commons.csv.Constants.CR;
 import static org.apache.commons.csv.Constants.END_OF_STREAM;
@@ -200,7 +202,7 @@ boolean isStartOfLine(final int ch) {
         return ch == LF || ch == CR || ch == UNDEFINED;
     }
 
-    private char mapNullToDisabled(final @Nulable Character c) {
+    private char mapNullToDisabled(@UnknownInitialization Lexer this, final @Nullable Character c) {
         return c == null ? DISABLED : c.charValue();
     }