diff --git a/count-issues b/count-issues new file mode 100755 index 0000000..f86bb76 --- /dev/null +++ b/count-issues @@ -0,0 +1,22 @@ +#!/bin/bash + +set -e + +read-and-count-issues() { + issues="$(grep -e "^\\[WARNING\\] .*.java:\\[\\d\+,\\d\+\\]" | \ + sed -E 's/^\[WARNING\] .*.java:\[[0-9,]+\] \[//g;s/\].*$//' | \ + sort)" + echo "$issues" | uniq -c + printf "%4d [TOTAL]\n" "$(echo "$issues" | wc -l)" +} + +SCRIPT_DIR=$( cd -- "$( dirname -- "${BASH_SOURCE[0]}" )" &> /dev/null && pwd ) + +echo "Before refactoring:" +cat "$SCRIPT_DIR/before-refactor.txt" | read-and-count-issues +echo "" + +cd "$SCRIPT_DIR/sources" +mvn clean 2>&1 >/dev/null +echo "After refactoring:" +mvn compile 2>&1 | read-and-count-issues diff --git a/sources/src/main/java/org/apache/commons/text/translate/AggregateTranslator.java b/sources/src/main/java/org/apache/commons/text/translate/AggregateTranslator.java index ac9aa0a..281bcef 100644 --- a/sources/src/main/java/org/apache/commons/text/translate/AggregateTranslator.java +++ b/sources/src/main/java/org/apache/commons/text/translate/AggregateTranslator.java @@ -18,6 +18,7 @@ package org.apache.commons.text.translate; import org.checkerframework.checker.index.qual.LTLengthOf; import org.checkerframework.checker.index.qual.NonNegative; +import org.checkerframework.common.value.qual.MinLen; import java.io.IOException; import java.io.Writer; diff --git a/sources/src/main/java/org/apache/commons/text/translate/CharSequenceTranslator.java b/sources/src/main/java/org/apache/commons/text/translate/CharSequenceTranslator.java index f927b35..ef67c0e 100644 --- a/sources/src/main/java/org/apache/commons/text/translate/CharSequenceTranslator.java +++ b/sources/src/main/java/org/apache/commons/text/translate/CharSequenceTranslator.java @@ -26,6 +26,7 @@ import org.apache.commons.lang3.Validate; import org.checkerframework.checker.index.qual.LTLengthOf; import org.checkerframework.checker.index.qual.NonNegative; import org.checkerframework.checker.index.qual.Positive; +import org.checkerframework.common.value.qual.MinLen; /** * An API for translating text. @@ -83,7 +84,7 @@ public abstract class CharSequenceTranslator { * @return int count of code points consumed * @throws IOException if and only if the Writer produces an IOException */ - public abstract int translate(CharSequence input, + public abstract int translate(@MinLen(1) CharSequence input, @NonNegative @LTLengthOf("#1") int index, Writer writer) throws IOException; @@ -103,6 +104,7 @@ public abstract class CharSequenceTranslator { int pos = 0; final int len = input.length(); while (pos < len) { + assert input.length() >= 1 : "@AssumeAssertion(index): Trivially true since we enter the loop"; final int consumed = translate(input, pos, writer); if (consumed == 0) { // inlined implementation of Character.toChars(Character.codePointAt(input, pos)) diff --git a/sources/src/main/java/org/apache/commons/text/translate/CodePointTranslator.java b/sources/src/main/java/org/apache/commons/text/translate/CodePointTranslator.java index c6d482c..266fb6e 100644 --- a/sources/src/main/java/org/apache/commons/text/translate/CodePointTranslator.java +++ b/sources/src/main/java/org/apache/commons/text/translate/CodePointTranslator.java @@ -18,6 +18,7 @@ package org.apache.commons.text.translate; import org.checkerframework.checker.index.qual.LTLengthOf; import org.checkerframework.checker.index.qual.NonNegative; +import org.checkerframework.common.value.qual.MinLen; import java.io.IOException; import java.io.Writer; @@ -35,7 +36,7 @@ public abstract class CodePointTranslator extends CharSequenceTranslator { * {@inheritDoc} */ @Override - public final int translate(final CharSequence input, + public final int translate(final @MinLen(1) CharSequence input, final @NonNegative @LTLengthOf("#1") int index, final Writer writer) throws IOException { final int codePoint = Character.codePointAt(input, index); diff --git a/sources/src/main/java/org/apache/commons/text/translate/CsvTranslators.java b/sources/src/main/java/org/apache/commons/text/translate/CsvTranslators.java index 1751f59..1be864a 100644 --- a/sources/src/main/java/org/apache/commons/text/translate/CsvTranslators.java +++ b/sources/src/main/java/org/apache/commons/text/translate/CsvTranslators.java @@ -21,6 +21,7 @@ import java.io.Writer; import org.apache.commons.lang3.CharUtils; import org.apache.commons.lang3.StringUtils; +import org.checkerframework.common.value.qual.MinLen; /** * This class holds inner classes for escaping/unescaping Comma Separated Values. @@ -57,19 +58,14 @@ public final class CsvTranslators { public static class CsvUnescaper extends SinglePassTranslator { @Override - void translateWhole(final CharSequence input, final Writer writer) throws IOException { - final int zeroIndex = 0; + void translateWhole(final @MinLen(1) CharSequence input, final Writer writer) throws IOException { final int oneIndex = 1; final int lastIndex = input.length() - 1; - - // unfortunately there is no way to encode non-empty length - assert zeroIndex < input.length() && lastIndex >= 0 : - "@AssumeAssertion(index): translateWhole is called by " + - "SinglePassTranslator.translate(CharSequence, int, Writer), and that is part of a template method" + - "implementation that by contract is called only with non-empty `input` CharSequences"; + + assert lastIndex >= 0 : "@AssumeAssertion(index): input.length() is >= 1 by contract"; // is input not quoted? - if (input.charAt(zeroIndex) != CSV_QUOTE || input.charAt(lastIndex) != CSV_QUOTE) { + if (input.charAt(0) != CSV_QUOTE || input.charAt(lastIndex) != CSV_QUOTE) { writer.write(input.toString()); return; } diff --git a/sources/src/main/java/org/apache/commons/text/translate/SinglePassTranslator.java b/sources/src/main/java/org/apache/commons/text/translate/SinglePassTranslator.java index dd19ab5..b6d4ba9 100644 --- a/sources/src/main/java/org/apache/commons/text/translate/SinglePassTranslator.java +++ b/sources/src/main/java/org/apache/commons/text/translate/SinglePassTranslator.java @@ -16,6 +16,8 @@ */ package org.apache.commons.text.translate; +import org.checkerframework.common.value.qual.MinLen; + import java.io.IOException; import java.io.Writer; @@ -40,7 +42,7 @@ abstract class SinglePassTranslator extends CharSequenceTranslator { * @throws IllegalArgumentException if {@code index != 0} */ @Override - public int translate(final CharSequence input, final int index, final Writer writer) throws IOException { + public int translate(final @MinLen(1) CharSequence input, final int index, final Writer writer) throws IOException { if (index != 0) { throw new IllegalArgumentException(getClassName() + ".translate(final CharSequence input, final int " + "index, final Writer out) can not handle a non-zero index."); @@ -58,5 +60,5 @@ abstract class SinglePassTranslator extends CharSequenceTranslator { * @param writer Writer to translate the text to * @throws IOException if and only if the Writer produces an IOException */ - abstract void translateWhole(CharSequence input, Writer writer) throws IOException; + abstract void translateWhole(@MinLen(1) CharSequence input, Writer writer) throws IOException; }