Removing the @OptionalBottom type and annotation (#6772)

Co-authored-by: Michael Ernst <mernst@cs.washington.edu>
typetools · Sep 4, 2024 · 0aeb0a4 · 0aeb0a4
1 parent 87f9d44
commit 0aeb0a4
Show file tree

Hide file tree

Showing 5 changed files with 10 additions and 104 deletions.
diff --git a/checker-qual/src/main/java/org/checkerframework/checker/optional/qual/OptionalBottom.java b/checker-qual/src/main/java/org/checkerframework/checker/optional/qual/OptionalBottom.java
diff --git a/checker/tests/optional/SubtypeCheck.java b/checker/tests/optional/SubtypeCheck.java
@@ -1,27 +1,16 @@
 import java.util.Optional;
 import org.checkerframework.checker.optional.qual.MaybePresent;
-import org.checkerframework.checker.optional.qual.OptionalBottom;
 import org.checkerframework.checker.optional.qual.Present;
 
 /** Basic test of subtyping. */
 public class SubtypeCheck {
 
   @SuppressWarnings("optional.parameter")
-  void foo(
-      @MaybePresent Optional<String> mp,
-      @Present Optional<String> p,
-      @OptionalBottom Optional<String> ob) {
+  void foo(@MaybePresent Optional<String> mp, @Present Optional<String> p) {
     @MaybePresent Optional<String> mp2 = mp;
     @MaybePresent Optional<String> mp3 = p;
-    @MaybePresent Optional<String> mp4 = ob;
     // :: error: (assignment)
     @Present Optional<String> p2 = mp;
     @Present Optional<String> p3 = p;
-    @Present Optional<String> p4 = ob;
-    // :: error: (assignment)
-    @OptionalBottom Optional<String> ob2 = mp;
-    // :: error: (assignment)
-    @OptionalBottom Optional<String> ob3 = p;
-    @OptionalBottom Optional<String> ob4 = ob;
   }
 }
diff --git a/docs/CHANGELOG.md b/docs/CHANGELOG.md
@@ -1,13 +1,18 @@
-Version 3.46.1 (September 3, 2024)
+Version 3.47.0 (September 3, 2024)
 -----------------------------
 
 **User-visible changes:**
 
 The Checker Framework runs under JDK 22 -- that is, it runs on a version 22 JVM.
 The Checker Framework runs under JDK 23 -- that is, it runs on a version 23 JVM.
 
+The Optional Checker no longer supports the `@OptionalBottom` annotation.
+
 **Implementation details:**
 
+Removed annotations:
+  * `@OptionalBottom`
+
 **Closed issues:**
 
 

diff --git a/docs/manual/figures/optional-subtyping.svg b/docs/manual/figures/optional-subtyping.svg
diff --git a/docs/manual/optional-checker.tex b/docs/manual/optional-checker.tex
@@ -78,10 +78,6 @@
 \item[\refqualclass{checker/optional/qual}{Present}]
   The annotated \<Optional> container definitely contains a (non-null) value.
 
-\item[\refqualclass{checker/optional/qual}{OptionalBottom}]
-  The annotated expression evaluates to \<null> rather than to an \<Optional> container.
-  Programmers rarely write this annotation.
-
 \item[\refqualclass{checker/optional/qual}{PolyPresent}]
   indicates qualifier polymorphism.
   For a description of qualifier polymorphism, see