Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,7 @@
* <pre>
* {@literal @}Format({GENERAL, INT}) String f = "String '%s' has length %d";
*
* String.format(f, "Example", 7);
* String.format(f, "Example", 7);
* </pre>
*
* </blockquote>
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -14,9 +14,9 @@
* {@code String.indexOf(String)}</a> method is declared as
*
* <pre><code>
* class String {
* class String {
* {@literal @}IndexOrLow("this") int indexOf(String str) { ... }
* }
* }
* </code></pre>
*
* <p>Writing {@code @IndexOrLow("arr")} is equivalent to writing {@link
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -19,19 +19,19 @@
* effect:
*
* <pre><code>
* {@literal @}EnsuresNonEmpty("ids")
* void addId(String id) {
* ids.add(id);
* }
* {@literal @}EnsuresNonEmpty("ids")
* void addId(String id) {
* ids.add(id);
* }
* </code></pre>
*
* It can also be used for a method that fails if a given value is empty, indicating that the
* argument is non-empty if the method returns normally:
*
* <pre><code>
* /** Throws an exception if the argument is empty. *&#47;
* {@literal @}EnsuresNonEmpty("#1")
* void useTheMap(Map&lt;T, U&gt; arg) { ... }
* /** Throws an exception if the argument is empty. *&#47;
* {@literal @}EnsuresNonEmpty("#1")
* void useTheMap(Map&lt;T, U&gt; arg) { ... }
* </code></pre>
*
* @see NonEmpty
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -15,11 +15,11 @@
* <p>Here is an example use:
*
* <pre><code>
* {@literal @}AssertNonNullIfNonNull("id")
* {@literal @}Pure
* public @Nullable Long getId() {
* return id;
* }
* {@literal @}AssertNonNullIfNonNull("id")
* {@literal @}Pure
* public @Nullable Long getId() {
* return id;
* }
* </code></pre>
*
* Note the direction of the implication. This annotation says that if the result is non-null, then
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -16,19 +16,19 @@
* <p>This postcondition annotation is useful for methods that construct a present Optional:
*
* <pre><code>
* {@literal @}EnsuresPresent("optStr")
* void initialize() {
* optStr = Optional.of("abc");
* }
* {@literal @}EnsuresPresent("optStr")
* void initialize() {
* optStr = Optional.of("abc");
* }
* </code></pre>
*
* It can also be used for a method that fails if a given Optional value is empty, indicating that
* the argument is present if the method returns normally:
*
* <pre><code>
* /** Throws an exception if the argument is empty. *&#47;
* {@literal @}EnsuresPresent("#1")
* void useTheOptional(Optional&lt;T&gt; arg) { ... }
* /** Throws an exception if the argument is empty. *&#47;
* {@literal @}EnsuresPresent("#1")
* void useTheOptional(Optional&lt;T&gt; arg) { ... }
* </code></pre>
*
* @see Present
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -22,7 +22,7 @@
@Retention(RetentionPolicy.RUNTIME)
@Target({}) // empty target prevents programmers from writing this in a program
@InvisibleQualifier
@SubtypeOf(org.checkerframework.checker.regex.qual.UnknownRegex.class)
@SubtypeOf(UnknownRegex.class)
public @interface PartialRegex {

/**
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -23,6 +23,6 @@
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
@TargetLocations({TypeUseLocation.LOWER_BOUND, TypeUseLocation.UPPER_BOUND})
@InvisibleQualifier
@SubtypeOf({Regex.class, org.checkerframework.checker.regex.qual.PartialRegex.class})
@SubtypeOf({Regex.class, PartialRegex.class})
@DefaultFor(value = {TypeUseLocation.LOWER_BOUND})
public @interface RegexBottom {}
Original file line number Diff line number Diff line change
Expand Up @@ -33,16 +33,9 @@
TypeKind.FLOAT,
TypeKind.DOUBLE
},
types = {
java.lang.Byte.class,
java.lang.Integer.class,
java.lang.Long.class,
java.lang.Short.class,
java.lang.Float.class,
java.lang.Double.class
},
types = {Byte.class, Integer.class, Long.class, Short.class, Float.class, Double.class},
value = TypeUseLocation.EXCEPTION_PARAMETER)
@UpperBoundFor(
typeKinds = {TypeKind.FLOAT, TypeKind.DOUBLE},
types = {java.lang.Float.class, java.lang.Double.class})
types = {Float.class, Double.class})
public @interface Signed {}
Original file line number Diff line number Diff line change
Expand Up @@ -24,8 +24,8 @@
@SubtypeOf({UnknownSignedness.class})
@DefaultFor(
typeKinds = {TypeKind.CHAR},
types = {java.lang.Character.class})
types = {Character.class})
@UpperBoundFor(
typeKinds = {TypeKind.CHAR},
types = {java.lang.Character.class})
types = {Character.class})
public @interface Unsigned {}
Original file line number Diff line number Diff line change
Expand Up @@ -18,10 +18,10 @@
* <p>Here is an example use:
*
* <pre><code>
* {@literal @}EnsuresQualifierIf(result = true, expression = "#1", qualifier = Odd.class)
* boolean isOdd(int p1, int p2) {
* return p1 % 2 == 1;
* }
* {@literal @}EnsuresQualifierIf(result = true, expression = "#1", qualifier = Odd.class)
* boolean isOdd(int p1, int p2) {
* return p1 % 2 == 1;
* }
* </code></pre>
*
* <p>This annotation is only applicable to methods with a boolean return type.
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -31,8 +31,8 @@
* org.checkerframework.common.value.qual.MinLen} qualifier:
*
* <pre><code>
* {@literal @}PostconditionAnnotation(qualifier = MinLen.class)
* {@literal @}Target({ElementType.METHOD, ElementType.CONSTRUCTOR})
* {@literal @}PostconditionAnnotation(qualifier = MinLen.class)
* {@literal @}Target({ElementType.METHOD, ElementType.CONSTRUCTOR})
* public {@literal @}interface EnsuresMinLen {
* String[] value();
* {@literal @}QualifierArgument("value")
Expand All @@ -47,7 +47,7 @@
* {@code @MinLen(2)} upon return.
*
* <pre><code>
* {@literal @}EnsuresMinLen(value = "field", targetValue = 2")
* {@literal @}EnsuresMinLen(value = "field", targetValue = 2)
* public void setField(String argument) {
* field = "(" + argument + ")";
* }
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -27,12 +27,12 @@
* org.checkerframework.common.value.qual.MinLen} qualifier:
*
* <pre><code>
* {@literal @}PreconditionAnnotation(qualifier = MinLen.class)
* {@literal @}Target({ElementType.METHOD, ElementType.CONSTRUCTOR})
* public {@literal @}interface RequiresMinLen {
* String[] value();
* {@literal @}QualifierArgument("value")
* int targetValue() default 0;
* {@literal @}PreconditionAnnotation(qualifier = MinLen.class)
* {@literal @}Target({ElementType.METHOD, ElementType.CONSTRUCTOR})
* public {@literal @}interface RequiresMinLen {
* String[] value();
* {@literal @}QualifierArgument("value")
* int targetValue() default 0;
* </code></pre>
*
* The {@code value} element holds the expressions to which the qualifier applies and {@code
Expand All @@ -43,10 +43,10 @@
* {@code @MinLen(2)} upon entry.
*
* <pre><code>
* {@literal @}RequiresMinLen(value = "field", targetValue = 2")
* public char getThirdCharacter() {
* return field.charAt(2);
* }
* {@literal @}RequiresMinLen(value = "field", targetValue = 2")
* public char getThirdCharacter() {
* return field.charAt(2);
* }
* </code></pre>
*
* @see RequiresQualifier
Expand Down
Loading