Add annotations that were not copied from jdk8 (openjdk#7)

Note: the annotations added to src/java.base/share/classes/java/util/Properties.java are to methods that are new JDK 11.

Author: smillst

src/java.base/share/classes/java/util/Optional.java

@@ -24,9 +24,16 @@
  */
 package java.util;
 
+import org.checkerframework.checker.nullness.qual.PolyNull;
+import org.checkerframework.checker.nullness.qual.Nullable;
+import org.checkerframework.checker.nullness.qual.NonNull;
 import org.checkerframework.framework.qual.AnnotatedFor;
+import org.checkerframework.framework.qual.Covariant;
 import org.checkerframework.framework.qual.CFComment;
 
+import org.checkerframework.checker.optional.qual.Present;
+import org.checkerframework.framework.qual.EnsuresQualifierIf;
+
 import java.util.function.Consumer;
 import java.util.function.Function;
 import java.util.function.Predicate;
@@ -71,8 +78,9 @@
 "meaning, but are unrelated by the Java type hierarchy.",
 "@Covariant makes Optional<@NonNull String> a subtype of Optional<@Nullable String>."
 })
-@AnnotatedFor({"lock", "nullness"})
-public final class Optional<T> {
+@AnnotatedFor({"lock", "nullness", "optional"})
+@Covariant(0)
+public final @NonNull class Optional<T> {
     /**
      * Common instance for {@code empty()}.
      */
@@ -81,7 +89,7 @@ public final class Optional<T> {
     /**
      * If non-null, the value; if null, indicates no value is present
      */
-    private final T value;
+    private final @Nullable T value;
 
     /**
      * Constructs an empty instance.
@@ -118,7 +126,7 @@ public static<T> Optional<T> empty() {
      * @param value the non-{@code null} value to describe
      * @throws NullPointerException if value is {@code null}
      */
-    private Optional(T value) {
+    private Optional(@NonNull T value) {
         this.value = Objects.requireNonNull(value);
     }
 
@@ -131,7 +139,7 @@ private Optional(T value) {
      * @return an {@code Optional} with the value present
      * @throws NullPointerException if value is {@code null}
      */
-    public static <T> Optional<T> of(T value) {
+    public static <T> @Present Optional<T> of(@NonNull T value) {
         return new Optional<>(value);
     }
 
@@ -144,7 +152,7 @@ public static <T> Optional<T> of(T value) {
      * @return an {@code Optional} with a present value if the specified value
      *         is non-{@code null}, otherwise an empty {@code Optional}
      */
-    public static <T> Optional<T> ofNullable(T value) {
+    public static <T> Optional<T> ofNullable(@Nullable T value) {
         return value == null ? empty() : of(value);
     }
 
@@ -158,7 +166,7 @@ public static <T> Optional<T> ofNullable(T value) {
      * @return the non-{@code null} value described by this {@code Optional}
      * @throws NoSuchElementException if no value is present
      */
-    public T get() {
+    public @NonNull T get(@Present Optional<T> this) {
         if (value == null) {
             throw new NoSuchElementException("No value present");
         }
@@ -170,6 +178,7 @@ public T get() {
      *
      * @return {@code true} if a value is present, otherwise {@code false}
      */
+    @EnsuresQualifierIf(result = true, expression = "this", qualifier = Present.class)
     public boolean isPresent() {
         return value != null;
     }
@@ -272,7 +281,7 @@ public Optional<T> filter(Predicate<? super T> predicate) {
      *         present, otherwise an empty {@code Optional}
      * @throws NullPointerException if the mapping function is {@code null}
      */
-    public <U> Optional<U> map(Function<? super T, ? extends U> mapper) {
+    public <U> Optional<U> map(Function<? super T, ? extends @Nullable U> mapper) {
         Objects.requireNonNull(mapper);
         if (!isPresent()) {
             return empty();
@@ -366,7 +375,7 @@ public Stream<T> stream() {
      *        May be {@code null}.
      * @return the value, if present, otherwise {@code other}
      */
-    public T orElse(T other) {
+    public @PolyNull T orElse(@PolyNull T other) {
         return value != null ? value : other;
     }
 
@@ -380,7 +389,7 @@ public T orElse(T other) {
      * @throws NullPointerException if no value is present and the supplying
      *         function is {@code null}
      */
-    public T orElseGet(Supplier<? extends T> supplier) {
+    public @PolyNull T orElseGet(Supplier<? extends @PolyNull T> supplier) {
         return value != null ? value : supplier.get();
     }
 
@@ -416,7 +425,7 @@ public T orElseThrow() {
      * @throws NullPointerException if no value is present and the exception
      *          supplying function is {@code null}
      */
-    public <X extends Throwable> T orElseThrow(Supplier<? extends X> exceptionSupplier) throws X {
+    public <X extends Throwable> T orElseThrow(@Present Optional<T> this, Supplier<? extends X> exceptionSupplier) throws X {
         if (value != null) {
             return value;
         } else {

src/java.base/share/classes/java/util/Properties.java

@@ -26,6 +26,7 @@
 package java.util;
 
 import org.checkerframework.checker.lock.qual.GuardSatisfied;
+import org.checkerframework.checker.nullness.qual.KeyFor;
 import org.checkerframework.checker.nullness.qual.Nullable;
 import org.checkerframework.checker.nullness.qual.PolyNull;
 import org.checkerframework.checker.propkey.qual.PropertyKey;
@@ -1347,7 +1348,7 @@ public synchronized String toString() {
     }
 
     @Override
-    public Set<Object> keySet() {
+    public Set<@KeyFor("this") Object> keySet() {
         return Collections.synchronizedSet(map.keySet(), this);
     }
 
@@ -1357,7 +1358,7 @@ public Collection<Object> values() {
     }
 
     @Override
-    public Set<Map.Entry<Object, Object>> entrySet() {
+    public Set<Map.Entry<@KeyFor("this") Object, Object>> entrySet() {
         return Collections.synchronizedSet(new EntrySet(map.entrySet()), this);
     }
 

src/java.base/share/classes/java/util/ResourceBundle.java

@@ -40,6 +40,7 @@
 
 package java.util;
 
+import org.checkerframework.checker.index.qual.NonNegative;
 import org.checkerframework.checker.i18n.qual.LocalizableKey;
 import org.checkerframework.checker.i18n.qual.Localized;
 import org.checkerframework.checker.i18nformatter.qual.I18nMakeFormat;
@@ -3307,7 +3308,7 @@ public InputStream run() throws IOException {
          *        if <code>baseName</code> or <code>locale</code> is
          *        <code>null</code>
          */
-        public long getTimeToLive(String baseName, Locale locale) {
+        public @NonNegative long getTimeToLive(String baseName, Locale locale) {
             if (baseName == null || locale == null) {
                 throw new NullPointerException();
             }