| package org.checkerframework.checker.index.qual; |
| |
| import java.lang.annotation.Documented; |
| import java.lang.annotation.ElementType; |
| import java.lang.annotation.Retention; |
| import java.lang.annotation.RetentionPolicy; |
| import java.lang.annotation.Target; |
| import org.checkerframework.framework.qual.JavaExpression; |
| import org.checkerframework.framework.qual.SubtypeOf; |
| |
| /** |
| * The annotated expression evaluates to either -1 or a non-negative integer less than the lengths |
| * of all the given sequences. The annotation {@code @SubstringIndexFor(args)} is like <code> |
| * {@literal @}{@link NonNegative} {@literal @}{@link LTLengthOf}(args)</code>, except that |
| * {@code @SubstringIndexFor(args)} additionally permits the value -1. |
| * |
| * <p>When multiple values or offsets are given, they are considered pairwise. For example, |
| * {@code @SubstringIndexFor(value={"a", "b"}, offset={"c", "d"})} is equivalent to writing both |
| * {@code @SubstringIndexFor(value="a", offset="c")} and {@code @SubstringIndexFor(value="b", |
| * offset="d")}. |
| * |
| * <p>The return types of JDK methods {@link java.lang.String#indexOf(String) String.indexOf} and |
| * {@link java.lang.String#lastIndexOf(String) String.lastIndexOf} are annotated |
| * {@code @SubstringIndexFor(value="this",offset="#1.length()-1")}. This means that the returned |
| * value is either -1 or it is less than or equal to the length of the receiver sequence minus the |
| * length of the sequence passed as the first argument. |
| * |
| * <p>The name of this annotation, "substring index for", is intended to mean that the annotated |
| * expression is a index of a substring (returned by {@code indexOf} or similar methods) for the |
| * specified sequence. |
| * |
| * @checker_framework.manual #index-substringindex Index Checker |
| */ |
| @Documented |
| @Retention(RetentionPolicy.RUNTIME) |
| @Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER}) |
| @SubtypeOf(SubstringIndexUnknown.class) |
| public @interface SubstringIndexFor { |
| /** |
| * Sequences, each of which is longer than the annotated expression plus the corresponding {@code |
| * offset}. (Exception: the annotated expression is also allowed to have the value -1.) |
| */ |
| @JavaExpression |
| public String[] value(); |
| |
| /** |
| * This expression plus the annotated expression is less than the length of the corresponding |
| * sequence in the {@code value} array. (Exception: the annotated expression is also allowed to |
| * have the value -1.) |
| * |
| * <p>The {@code offset} array must either be empty or the same length as {@code value}. |
| * |
| * <p>The expressions in {@code offset} may be addition/subtraction of any number of Java |
| * expressions. For example, {@code @SubstringIndexFor(value = "a", offset = "b.length() - 1")}. |
| */ |
| @JavaExpression |
| public String[] offset(); |
| } |