-
Notifications
You must be signed in to change notification settings - Fork 350
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Merge branch 'master' into custom-list-of-ignored-rlc-exceptions
- Loading branch information
Showing
60 changed files
with
2,027 additions
and
200 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
49 changes: 49 additions & 0 deletions
49
checker-qual/src/main/java/org/checkerframework/checker/optional/qual/EnsuresPresent.java
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,49 @@ | ||
package org.checkerframework.checker.optional.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.InheritedAnnotation; | ||
import org.checkerframework.framework.qual.PostconditionAnnotation; | ||
|
||
/** | ||
* Indicates that the expression evaluates to a non-empty Optional, if the method terminates | ||
* successfully. | ||
* | ||
* <p>This postcondition annotation is useful for methods that construct a non-empty Optional: | ||
* | ||
* <pre><code> | ||
* {@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 null if the method returns normally: | ||
* | ||
* <pre><code> | ||
* /** Throws an exception if the argument is empty. */ | ||
* {@literal @}EnsuresPresent("#1") | ||
* void useTheOptional(Optional<T> arg) { ... } | ||
* </code></pre> | ||
* | ||
* @see Present | ||
* @see org.checkerframework.checker.optional.OptionalChecker | ||
* @checker_framework.manual #optional-checker Optional Checker | ||
*/ | ||
@Documented | ||
@Retention(RetentionPolicy.RUNTIME) | ||
@Target({ElementType.METHOD, ElementType.CONSTRUCTOR}) | ||
@PostconditionAnnotation(qualifier = Present.class) | ||
@InheritedAnnotation | ||
public @interface EnsuresPresent { | ||
/** | ||
* The expression (of Optional type) that is present, if the method returns normally. | ||
* | ||
* @return the expression (of Optional type) that is present, if the method returns normally | ||
*/ | ||
String[] value(); | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
75 changes: 75 additions & 0 deletions
75
checker-util/src/main/java/org/checkerframework/checker/optional/util/OptionalUtil.java
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,75 @@ | ||
package org.checkerframework.checker.optional.util; | ||
|
||
import java.util.Optional; | ||
import org.checkerframework.checker.optional.qual.EnsuresPresent; | ||
import org.checkerframework.checker.optional.qual.MaybePresent; | ||
import org.checkerframework.checker.optional.qual.Present; | ||
import org.checkerframework.framework.qual.AnnotatedFor; | ||
|
||
/** | ||
* This is a utility class for the Optional Checker. | ||
* | ||
* <p>To avoid the need to write the OptionalUtil class name, do: | ||
* | ||
* <pre>import static org.checkerframework.checker.optional.util.OptionalUtil.castPresent;</pre> | ||
* | ||
* or | ||
* | ||
* <pre>import static org.checkerframework.checker.optional.util.OptionalUtil.*;</pre> | ||
* | ||
* <p><b>Runtime Dependency</b>: If you use this class, you must distribute (or link to) {@code | ||
* checker-qual.jar}, along with your binaries. Or, you can copy this class into your own project. | ||
*/ | ||
@SuppressWarnings({ | ||
"optional", // Optional utilities are trusted regarding the Optional type. | ||
"cast" // Casts look redundant if Optional Checker is not run. | ||
}) | ||
@AnnotatedFor("optional") | ||
public final class OptionalUtil { | ||
|
||
/** The OptionalUtil class should not be instantiated. */ | ||
private OptionalUtil() { | ||
throw new AssertionError("do not instantiate"); | ||
} | ||
|
||
/** | ||
* A method that suppresses warnings from the Optional Checker. | ||
* | ||
* <p>The method takes a possibly-empty Optional reference, unsafely casts it to have the @Present | ||
* type qualifier, and returns it. The Optional Checker considers both the return value, and also | ||
* the argument, to be present after the method call. Therefore, the {@code castPresent} method | ||
* can be used either as a cast expression or as a statement. | ||
* | ||
* <pre><code> | ||
* // one way to use as a cast: | ||
* {@literal @}Present String s = castPresent(possiblyEmpty1); | ||
* | ||
* // another way to use as a cast: | ||
* castPresent(possiblyEmpty2).toString(); | ||
* | ||
* // one way to use as a statement: | ||
* castPresent(possiblyEmpty3); | ||
* possiblyEmpty3.toString(); | ||
* </code></pre> | ||
* | ||
* The {@code castPresent} method is intended to be used in situations where the programmer | ||
* definitively knows that a given Optional reference is present, but the type system is unable to | ||
* make this deduction. It is not intended for defensive programming, in which a programmer cannot | ||
* prove that the value is not empty but wishes to have an earlier indication if it is. See the | ||
* Checker Framework Manual for further discussion. | ||
* | ||
* <p>The method throws {@link AssertionError} if Java assertions are enabled and the argument is | ||
* empty. If the exception is ever thrown, then that indicates that the programmer misused the | ||
* method by using it in a circumstance where its argument can be empty. | ||
* | ||
* @param <T> the type of content of the Optional | ||
* @param ref an Optional reference of @MaybePresent type, that is present at run time | ||
* @return the argument, casted to have the type qualifier @Present | ||
*/ | ||
@EnsuresPresent("#1") | ||
public static <T extends @MaybePresent Object> @Present Optional<T> castPresent( | ||
@MaybePresent Optional<T> ref) { | ||
assert ref.isPresent() : "Misuse of castPresent: called with an empty Optional"; | ||
return (@Present Optional<T>) ref; | ||
} | ||
} |
23 changes: 23 additions & 0 deletions
23
checker-util/src/test/java/org/checkerframework/checker/optional/util/OptionalUtilTest.java
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,23 @@ | ||
package org.checkerframework.checker.optional.util; | ||
|
||
import java.util.Optional; | ||
import org.checkerframework.checker.optional.qual.Present; | ||
import org.junit.Assert; | ||
import org.junit.Test; | ||
|
||
public final class OptionalUtilTest { | ||
|
||
@Test | ||
public void test_castPresent() { | ||
|
||
Optional<String> nonEmptyOpt = Optional.of("non-empty"); | ||
Optional<String> emptyOpt = Optional.empty(); | ||
|
||
Assert.assertFalse(nonEmptyOpt.isEmpty()); | ||
@Present Optional<String> foo = OptionalUtil.castPresent(nonEmptyOpt); | ||
Assert.assertEquals(foo.get(), "non-empty"); | ||
|
||
Assert.assertTrue(emptyOpt.isEmpty()); | ||
Assert.assertThrows(Error.class, () -> OptionalUtil.castPresent(emptyOpt)); | ||
} | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.