diff --git a/sources/src/main/java/org/apache/commons/text/AlphabetConverter.java b/sources/src/main/java/org/apache/commons/text/AlphabetConverter.java index 033ede1..9d47ea3 100644 --- a/sources/src/main/java/org/apache/commons/text/AlphabetConverter.java +++ b/sources/src/main/java/org/apache/commons/text/AlphabetConverter.java @@ -31,6 +31,7 @@ import java.util.Set; import org.apache.commons.lang3.ArrayUtils; import org.apache.commons.lang3.StringUtils; +import org.checkerframework.checker.index.qual.NonNegative; /** *
@@ -104,7 +105,12 @@ public final class AlphabetConverter {
return ArrayUtils.EMPTY_INTEGER_OBJECT_ARRAY;
}
final Integer[] integers = new Integer[chars.length];
- Arrays.setAll(integers, i -> (int) chars[i]);
+ Arrays.setAll(integers, i -> {
+ assert i >= 0 && i < chars.length : "@AssumeAssertion(index): i is a valid index for integers, and integers" +
+ "has same length of chars";
+
+ return (int) chars[i];
+ });
return integers;
}
@@ -384,7 +390,7 @@ public final class AlphabetConverter {
final StringBuilder result = new StringBuilder();
- for (int j = 0; j < encoded.length();) {
+ for (@NonNegative int j = 0; j < encoded.length();) {
final int i = encoded.codePointAt(j);
final String s = codePointToString(i);
@@ -393,6 +399,9 @@ public final class AlphabetConverter {
j++; // because we do not encode in Unicode extended the
// length of each encoded char is 1
} else {
+ assert encodedLetterLength >= 0 : "@AssumeAssertion(index): follows from constructor contract of " +
+ "AlphabetConverter";
+
if (j + encodedLetterLength > encoded.length()) {
throw new UnsupportedEncodingException("Unexpected end "
+ "of string while decoding " + encoded);
diff --git a/sources/src/main/java/org/apache/commons/text/StringSubstitutor.java b/sources/src/main/java/org/apache/commons/text/StringSubstitutor.java
index 3b1e4cb..4c5ce94 100644
--- a/sources/src/main/java/org/apache/commons/text/StringSubstitutor.java
+++ b/sources/src/main/java/org/apache/commons/text/StringSubstitutor.java
@@ -29,6 +29,7 @@ import org.apache.commons.text.lookup.StringLookup;
import org.apache.commons.text.lookup.StringLookupFactory;
import org.apache.commons.text.matcher.StringMatcher;
import org.apache.commons.text.matcher.StringMatcherFactory;
+import org.checkerframework.checker.index.qual.*;
/**
* Substitutes variables within a string by values.
@@ -914,7 +915,9 @@ public class StringSubstitutor {
* @throws StringIndexOutOfBoundsException if {@code length < 0}
* @throws StringIndexOutOfBoundsException if {@code offset + length > source.length()}
*/
- public String replace(final String source, final int offset, final int length) {
+ public String replace(final String source,
+ final @IndexOrHigh("#1") int offset,
+ final @NonNegative @LTLengthOf(value = "#1", offset = "#2 - 1") int length) {
if (source == null) {
return null;
}
diff --git a/sources/src/main/java/org/apache/commons/text/similarity/LongestCommonSubsequence.java b/sources/src/main/java/org/apache/commons/text/similarity/LongestCommonSubsequence.java
index b91f23c..406181d 100644
--- a/sources/src/main/java/org/apache/commons/text/similarity/LongestCommonSubsequence.java
+++ b/sources/src/main/java/org/apache/commons/text/similarity/LongestCommonSubsequence.java
@@ -86,6 +86,8 @@ public class LongestCommonSubsequence implements SimilarityScore